(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Properties in Topology 3› theory Topology_ZF_properties_3 imports Topology_ZF_7 Finite_ZF_1 Topology_ZF_1b Topology_ZF_9 Topology_ZF_properties_2 FinOrd_ZF begin text‹This theory file deals with more topological properties and the relation with the previous ones in other theory files.› subsection‹More anti-properties› text‹In this section we study more anti-properties.› subsection‹First examples› text‹A first example of an anti-compact space is the discrete space.› lemma pow_compact_imp_finite: assumes "B{is compact in}Pow(A)" shows "Finite(B)" proof- from assms have B:"B⊆A" "∀M∈Pow(Pow(A)). B⊆⋃M ⟶(∃N∈FinPow(M). B⊆⋃N)" unfolding IsCompact_def by auto from B(1) have "{{x}. x∈B}∈Pow(Pow(A))" "B⊆⋃{{x}. x∈B}" by auto with B(2) have "∃N∈FinPow({{x}. x∈B}). B⊆⋃N" by auto then obtain N where "N∈FinPow({{x}. x∈B})" "B⊆⋃N" by auto then have "Finite(N)" "N⊆{{x}. x∈B}" "B⊆⋃N" unfolding FinPow_def by auto then have "Finite(N)" "∀b∈N. Finite(b)" "B⊆⋃N" by auto then have "B⊆⋃N" "Finite(⋃N)" using Finite_Union[of "N"] by auto then show "Finite(B)" using subset_Finite by auto qed theorem pow_anti_compact: shows "Pow(A){is anti-compact}" proof- { fix B assume as:"B⊆⋃Pow(A)" "(⋃(Pow(A){restricted to}B)){is compact in}(Pow(A){restricted to}B)" then have sub:"B⊆A" by auto then have "Pow(B)=Pow(A){restricted to}B" unfolding RestrictedTo_def by blast with as(2) have "(⋃Pow(B)){is compact in}Pow(B)" by auto then have "B{is compact in}Pow(B)" by auto then have "Finite(B)" using pow_compact_imp_finite by auto then have "B{is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto } then show ?thesis unfolding IsAntiComp_def antiProperty_def by auto qed text‹In a previous file, @{file "Topology_ZF_5.thy"}, we proved that the spectrum of the lindelöf property depends on the axiom of countable choice on subsets of the power set of the natural number.› text‹In this context, the examples depend on wether this choice principle holds or not. This is the reason that the examples of anti-lindeloef topologies are left for the next section.› subsection‹Structural results› text‹We first differenciate the spectrum of the lindeloef property depending on some axiom of choice.› lemma lindeloef_spec1: assumes "{the axiom of} nat {choice holds for subsets}(Pow(nat))" shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ (A≲nat)" using compactK_spectrum[OF assms Card_nat] unfolding IsLindeloef_def. lemma lindeloef_spec2: assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)))" shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ Finite(A)" proof assume "Finite(A)" then have A:"A{is in the spectrum of} (λT. ((⋃T){is compact in}T))" using compact_spectrum by auto have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto { fix T assume "T{is a topology}" "(⋃T){is compact in}T" then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto } then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto with A show "A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using P_imp_Q_spec_inv[ where Q="λT. ((⋃T){is compact in}T)" and P="λT. ((⋃T){is lindeloef in}T)"] by auto next assume A:"A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" then have reg:"∀T. T{is a topology}∧⋃T≈A ⟶ ((⋃T){is compact of cardinal} csucc(nat){in}T)" using Spec_def unfolding IsLindeloef_def by auto then have "A{is compact of cardinal} csucc(nat) {in} Pow(A)" using Pow_is_top[of "A"] by auto then have "∀M∈Pow(Pow(A)). A⊆⋃M ⟶ (∃N∈Pow(M). A⊆⋃N ∧ N≺csucc(nat))" unfolding IsCompactOfCard_def by auto moreover have "{{x}. x∈A}∈Pow(Pow(A))" by auto moreover have "A=⋃{{x}. x∈A}" by auto ultimately have "∃N∈Pow({{x}. x∈A}). A⊆⋃N ∧ N≺csucc(nat)" by auto then obtain N where "N∈Pow({{x}. x∈A})" "A⊆⋃N" "N≺csucc(nat)" by auto then have "N⊆{{x}. x∈A}" "N≺csucc(nat)" "A⊆⋃N" using FinPow_def by auto { fix t assume "t∈{{x}. x∈A}" then obtain x where "x∈A""t={x}" by auto with ‹A⊆⋃N› have "x∈⋃N" by auto then obtain B where "B∈N""x∈B" by auto with ‹N⊆{{x}. x∈A}› have "B={x}" by auto with ‹t={x}›‹B∈N› have "t∈N" by auto } with ‹N⊆{{x}. x∈A}› have "N={{x}. x∈A}" by auto let ?B="{⟨x,{x}⟩. x∈A}" from ‹N={{x}. x∈A}› have "?B:A→ N" unfolding Pi_def function_def by auto with ‹N={{x}. x∈A}› have "?B:inj(A,N)" unfolding inj_def using apply_equality by auto then have "A≲N" using lepoll_def by auto with ‹N≺csucc(nat)› have "A≺csucc(nat)" using lesspoll_trans1 by auto then have "A≲nat" using Card_less_csucc_eq_le Card_nat by auto then have "A≺nat∨A≈nat" using lepoll_iff_leqpoll by auto moreover { assume "A≈nat" then have "nat≈A" using eqpoll_sym by auto with A have "nat {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using equipollent_spect[ where P="(λT. ((⋃T){is lindeloef in}T))"] by auto moreover have "Pow(nat){is a topology}" using Pow_is_top by auto moreover have "⋃Pow(nat)=nat" by auto then have "⋃Pow(nat)≈nat" using eqpoll_refl by auto ultimately have "nat {is compact of cardinal} csucc(nat){in}Pow(nat)" using Spec_def unfolding IsLindeloef_def by auto then have "False" using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ[OF InfCard_nat] assms by auto } ultimately have "A≺nat" by auto then show "Finite(A)" using lesspoll_nat_is_Finite by auto qed text‹If the axiom of countable choice on subsets of the pow of the natural numbers doesn't hold, then anti-lindeloef spaces are anti-compact.› theorem(in topology0) no_choice_imp_anti_lindeloef_is_anti_comp: assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)) )" "T{is anti-lindeloef}" shows "T{is anti-compact}" proof- have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto { fix T assume "T{is a topology}" "(⋃T){is compact in}T" then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto } then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto from eq_spect_rev_imp_anti[OF this] lindeloef_spec2[OF assms(1)] compact_spectrum show ?thesis using assms(2) unfolding IsAntiLin_def IsAntiComp_def by auto qed text‹If the axiom of countable choice holds for subsets of the power set of the natural numbers, then there exists a topological space that is anti-lindeloef but no anti-compact.› theorem no_choice_imp_anti_lindeloef_is_anti_comp: assumes "({the axiom of} nat {choice holds for subsets}(Pow(nat)))" shows "({one-point compactification of}Pow(nat)){is anti-lindeloef}" proof- have t:"⋃({one-point compactification of}Pow(nat))={nat}∪nat" using topology0.op_compact_total unfolding topology0_def using Pow_is_top by auto have "{nat}≈1" using singleton_eqpoll_1 by auto then have "{nat}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto ultimately have "{nat}≺csucc(nat)" using lesspoll_trans by blast with s have "{nat}∪nat≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]] by auto then have "{nat}∪nat≲nat" using Card_less_csucc_eq_le[OF Card_nat] by auto with t have r:"⋃({one-point compactification of}Pow(nat))≲nat" by auto { fix A assume A:"A∈Pow(⋃({one-point compactification of}Pow(nat)))" "(⋃(({one-point compactification of}Pow(nat)){restricted to}A)){is lindeloef in}(({one-point compactification of}Pow(nat)){restricted to}A)" from A(1) have "A⊆⋃({one-point compactification of}Pow(nat))" by auto with r have "A≲nat" using subset_imp_lepoll lepoll_trans by blast then have "A{is in the spectrum of}(λT. ((⋃T){is lindeloef in}T))" using assms lindeloef_spec1 by auto } then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto qed theorem op_comp_pow_nat_no_anti_comp: shows "¬(({one-point compactification of}Pow(nat)){is anti-compact})" proof let ?T="({one-point compactification of}Pow(nat)){restricted to}({nat} ∪ nat)" assume antiComp:"({one-point compactification of}Pow(nat)){is anti-compact}" have "({nat} ∪ nat){is compact in}({one-point compactification of}Pow(nat))" using topology0.compact_op[of "Pow(nat)"] Pow_is_top[of "nat"] unfolding topology0_def by auto then have "({nat} ∪ nat){is compact in}?T" using compact_imp_compact_subspace Compact_is_card_nat by auto moreover have "⋃?T=(⋃({one-point compactification of}Pow(nat)))∩({nat} ∪ nat)" unfolding RestrictedTo_def by auto then have "⋃?T={nat} ∪ nat" using topology0.op_compact_total unfolding topology0_def using Pow_is_top by auto ultimately have "(⋃?T){is compact in}?T" by auto with antiComp have "({nat} ∪ nat){is in the spectrum of}(λT. (⋃T){is compact in}T)" unfolding IsAntiComp_def antiProperty_def using topology0.op_compact_total unfolding topology0_def using Pow_is_top by auto then have "Finite({nat} ∪ nat)" using compact_spectrum by auto then have "Finite(nat)" using subset_Finite by auto then show "False" using nat_not_Finite by auto qed text‹In coclusion, we reached another equivalence of this choice principle.› text‹The axiom of countable choice holds for subsets of the power set of the natural numbers if and only if there exists a topological space which is anti-lindeloef but not anti-compact; this space can be chosen as the one-point compactification of the discrete topology on $\mathbb{N}$.› theorem acc_pow_nat_equiv1: shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (({one-point compactification of}Pow(nat)){is anti-lindeloef})" using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top Pow_is_top[of "nat"] unfolding topology0_def by auto theorem acc_pow_nat_equiv2: shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (∃T. T{is a topology} ∧ (T{is anti-lindeloef}) ∧ ¬(T{is anti-compact}))" using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top Pow_is_top[of "nat"] unfolding topology0_def by auto text‹In the file @{file "Topology_ZF_properties.thy"}, it is proven that $\mathbb{N}$ is lindeloef if and only if the axiom of countable choice holds for subsets of $Pow(\mathbb{N})$. Now we check that, in ZF, this space is always anti-lindeloef.› theorem nat_anti_lindeloef: shows "Pow(nat){is anti-lindeloef}" proof- { fix A assume A:"A∈Pow(⋃Pow(nat))" "(⋃(Pow(nat){restricted to}A)){is lindeloef in}(Pow(nat){restricted to}A)" from A(1) have "A⊆nat" by auto then have "Pow(nat){restricted to}A=Pow(A)" unfolding RestrictedTo_def by blast with A(2) have lin:"A{is lindeloef in}Pow(A)" using subset_imp_lepoll by auto { fix T assume T:"T{is a topology}" "⋃T≈A" then have "A≈⋃T" using eqpoll_sym by auto then obtain f where f:"f∈bij(A,⋃T)" unfolding eqpoll_def by auto then have "f∈surj(A,⋃T)" unfolding bij_def by auto moreover then have "IsContinuous(Pow(A),T,f)" unfolding IsContinuous_def surj_def using func1_1_L3 by blast moreover have "two_top_spaces0(Pow(A),T,f)" unfolding two_top_spaces0_def using f T(1) Pow_is_top unfolding bij_def inj_def by auto ultimately have "(⋃T){is lindeloef in}T" using two_top_spaces0.cont_image_com lin unfolding IsLindeloef_def by auto } then have "A{is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" unfolding Spec_def by auto } then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto qed text‹This result is interesting because depending on the different axioms we add to ZF, it means two different things: \begin{itemize} \item Every subspace of $\mathbb{N}$ is Lindeloef. \item Only the compact subspaces of $\mathbb{N}$ are Lindeloef. \end{itemize} › text‹Now, we could wonder if the class of compact spaces and the class of lindeloef spaces being equal is consistent in ZF. Let's find a topological space which is lindeloef and no compact without assuming any axiom of choice or any negation of one. This will prove that the class of lindeloef spaces and the class of compact spaces cannot be equal in any model of ZF.› theorem lord_nat: shows "(LOrdTopology nat Le)={LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" proof- { fix U assume U:"U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" "U≠0" { assume "nat∈U" with U have "⋃U=nat" unfolding LeftRayX_def by auto then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}∪{0}" by auto } moreover { assume "nat∉U" with U have UU:"U⊆{LeftRayX(nat,Le,n). n∈nat}∪{0}" by auto { assume A:"∃i. i∈nat∧ ⋃U⊆ LeftRayX(nat,Le,i)" let ?M="μ i. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)" from A have M:"?M∈nat" "⋃U⊆ LeftRayX(nat,Le,?M)" using LeastI[OF _ nat_into_Ord, where P="λi. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)"] by auto { fix y assume V:"y∈LeftRayX(nat,Le,?M)" then have y:"y∈nat" unfolding LeftRayX_def by auto { assume "∀V∈U. y∉V" then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. y∉LeftRayX(nat,Le,m)" using UU by auto then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨y,m⟩∉Le∨y=m" unfolding LeftRayX_def using y by auto then have RR:"∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨m,y⟩∈Le" using Le_directs_nat(1) y unfolding IsLinOrder_def IsTotal_def by blast { fix rr V assume "rr∈⋃U" then obtain V where V:"V∈U" "rr∈V" by auto with UU obtain m where m:"V=LeftRayX(nat,Le,m)" "m∈nat" by auto with V(1) RR have a:"⟨m,y⟩∈Le" by auto from V(2) m(1) have b:"⟨rr,m⟩∈Le" "rr∈nat-{m}" unfolding LeftRayX_def by auto from a b(1) have "⟨rr,y⟩∈Le" using Le_directs_nat(1) unfolding IsLinOrder_def trans_def by blast moreover { assume "rr=y" with a b have "False" using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast } ultimately have "rr∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using b(2) by auto } then have "⋃U⊆LeftRayX(nat,Le,y)" by auto with y M(1) have "⟨?M,y⟩∈Le" using Least_le by auto with V have "False" unfolding LeftRayX_def using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast } then have "y∈⋃U" by auto } then have "LeftRayX(nat,Le,?M)⊆⋃U" by auto with M(2) have "⋃U=LeftRayX(nat,Le,?M)" by auto with M(1) have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" by auto } moreover { assume "¬(∃i. i ∈ nat ∧ ⋃U ⊆ LeftRayX(nat, Le, i))" then have A:"∀i. i∈nat ⟶ ¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto { fix i assume i:"i∈nat" with A have AA:"¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto { assume "i∉⋃U" then have "∀V∈U. i∉V" by auto then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. i∉LeftRayX(nat, Le, m)" by auto with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ⟨i,m⟩∉Le∨i=m" unfolding LeftRayX_def by auto with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ¬(i≤m)∨i=m" unfolding Le_def by auto then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m<i∨m=i" using not_le_iff_lt[OF nat_into_Ord[OF i] nat_into_Ord] by auto then have M:"∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m≤i" using le_iff nat_into_Ord[OF i] by auto { fix s assume "s∈⋃U" then obtain n where n:"n∈nat" "s∈LeftRayX(nat, Le, n)" "LeftRayX(nat, Le, n)∈U" using UU by auto with M have ni:"n≤i" by auto from n(2) have sn:"s≤n" "s≠n" unfolding LeftRayX_def by auto then have "s≤i" "s≠i" using le_trans[OF sn(1) ni] le_anti_sym[OF sn(1)] ni by auto then have "s∈LeftRayX(nat, Le, i)" using i le_in_nat unfolding LeftRayX_def by auto } with AA have "False" by auto } then have "i∈⋃U" by auto } then have "nat⊆⋃U" by auto then have "⋃U=nat" using UU unfolding LeftRayX_def by auto then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto } ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto } ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto } moreover { fix U assume "U=0" then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto } ultimately have "∀U. U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ⟶ ⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto then have "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}={⋃U. U∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat})}" by blast then show ?thesis using LOrdtopology_ROrdtopology_are_topologies(2)[OF Le_directs_nat(1)] unfolding IsAbaseFor_def by auto qed lemma countable_lord_nat: shows "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}≺csucc(nat)" proof- { fix e have "{e}≈1" using singleton_eqpoll_1 by auto then have "{e}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto ultimately have "{e}≺csucc(nat)" using lesspoll_trans by blast } then have "{nat} ∪{0}≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat], of "{nat}" "{0}"] by auto moreover let ?FF="{⟨n,LeftRayX(nat,Le,n)⟩. n∈nat}" have ff:"?FF:nat→{LeftRayX(nat,Le,n). n∈nat}" unfolding Pi_def domain_def function_def by auto then have su:"?FF∈surj(nat,{LeftRayX(nat,Le,n). n∈nat})" unfolding surj_def using apply_equality[ OF _ ff] by auto then have "{LeftRayX(nat,Le,n). n∈nat}≲nat" using surj_fun_inv_2[OF su lepoll_refl[of "nat"]] Ord_nat by auto then have "{LeftRayX(nat,Le,n). n∈nat}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto ultimately have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0}) ≺ csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]] by auto moreover have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0})={LeftRayX(nat, Le, n) . n ∈ nat} ∪ {nat} ∪ {0}" by auto ultimately show ?thesis by auto qed corollary lindelof_lord_nat: shows "nat{is lindeloef in}(LOrdTopology nat Le)" unfolding IsLindeloef_def using countable_lord_nat lord_nat card_top_comp[OF Card_csucc[OF Ord_nat]] union_lordtopology_rordtopology(1)[OF Le_directs_nat(1)] by auto theorem not_comp_lord_nat: shows "¬(nat{is compact in}(LOrdTopology nat Le))" proof assume "nat{is compact in}(LOrdTopology nat Le)" with lord_nat have "nat{is compact in}({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0})" by auto then have "∀M∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}). nat⊆⋃M ⟶ (∃N∈FinPow(M). nat⊆⋃N)" unfolding IsCompact_def by auto moreover { fix n assume n:"n∈nat" then have "n<succ(n)" by auto then have "⟨n,succ(n)⟩∈Le" "n≠succ(n)" using n nat_succ_iff by auto then have "n∈LeftRayX(nat,Le,succ(n))" unfolding LeftRayX_def using n by auto then have "n∈⋃({LeftRayX(nat,Le,n). n∈nat})" using n nat_succ_iff by auto } ultimately have "∃N∈FinPow({LeftRayX(nat,Le,n). n∈nat}). nat⊆⋃N" by blast then obtain N where "N∈FinPow({LeftRayX(nat,Le,n). n∈nat})" "nat⊆⋃N" by auto then have N:"N⊆{LeftRayX(nat,Le,n). n∈nat}" "Finite(N)" "nat⊆⋃N" unfolding FinPow_def by auto let ?F="{⟨n,LeftRayX(nat,Le,n)⟩. n∈{m∈nat. LeftRayX(nat,Le,m)∈N}}" have ff:"?F:{m∈nat. LeftRayX(nat,Le,m)∈N} → N" unfolding Pi_def function_def by auto then have "?F∈surj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding surj_def using N(1) apply_equality[ OF _ ff] by blast moreover { fix x y assume xyF:"x∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "y∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "?F`x=?F`y" then have "?F`x=LeftRayX(nat,Le,x)" "?F`y=LeftRayX(nat,Le,y)" using apply_equality[ OF _ ff] by auto with xyF(3) have lxy:"LeftRayX(nat,Le,x)=LeftRayX(nat,Le,y)" by auto { fix r assume "r<x" then have "r≤x" "r≠x" using leI by auto with xyF(1) have "r∈LeftRayX(nat,Le,x)" unfolding LeftRayX_def using le_in_nat by auto then have "r∈LeftRayX(nat,Le,y)" using lxy by auto then have "r≤y" "r≠y" unfolding LeftRayX_def by auto then have "r<y" using le_iff by auto } then have "∀r. r<x ⟶ r<y" by auto then have r:"¬(y<x)" by auto { fix r assume "r<y" then have "r≤y" "r≠y" using leI by auto with xyF(2) have "r∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using le_in_nat by auto then have "r∈LeftRayX(nat,Le,x)" using lxy by auto then have "r≤x" "r≠x" unfolding LeftRayX_def by auto then have "r<x" using le_iff by auto } then have "¬(x<y)" by auto with r have "x=y" using not_lt_iff_le[OF nat_into_Ord nat_into_Ord] xyF(1,2) le_anti_sym by auto } then have "?F∈inj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding inj_def using ff by auto ultimately have "?F∈bij({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding bij_def by auto then have "{m∈nat. LeftRayX(nat,Le,m)∈N}≈ N" unfolding eqpoll_def by auto with N(2) have fin:"Finite({m∈nat. LeftRayX(nat,Le,m)∈N})" using lepoll_Finite eqpoll_imp_lepoll by auto from N(3) have "N≠0" by auto then have nE:"{m∈nat. LeftRayX(nat,Le,m)∈N}≠0" using N(1) by auto let ?M="Maximum(Le,{m∈nat. LeftRayX(nat,Le,m)∈N})" have M:"?M∈nat" "LeftRayX(nat,Le,?M)∈N" "∀𝔵∈{m∈nat. LeftRayX(nat,Le,m)∈N}. ⟨𝔵,?M⟩∈Le" using fin linord_max_props(1,3)[OF Le_directs_nat(1) _ nE] unfolding FinPow_def by auto { fix V 𝔵 assume V:"V∈N" "𝔵∈V" then obtain m where m:"V=LeftRayX(nat,Le,m)" "LeftRayX(nat,Le,m)∈N" "m∈nat" using N(1) by auto with V(2) have xx:"⟨𝔵,m⟩∈Le" "𝔵≠m" unfolding LeftRayX_def by auto from m(2,3) have "m∈{m∈nat. LeftRayX(nat,Le,m)∈N}" by auto then have mM:"⟨m,?M⟩∈Le" using M(3) by auto with xx(1) have "⟨𝔵,?M⟩∈Le" using le_trans unfolding Le_def by auto moreover { assume "𝔵=?M" with xx mM have "False" using le_anti_sym by auto } ultimately have "𝔵∈LeftRayX(nat,Le,?M)" unfolding LeftRayX_def by auto } then have "⋃N⊆LeftRayX(nat,Le,?M)" by auto with M(2) have "⋃N=LeftRayX(nat,Le,?M)" by auto with N(3) have "nat⊆LeftRayX(nat,Le,?M)" by auto moreover from M(1) have "succ(?M)∈nat" using nat_succI by auto ultimately have "succ(?M)∈LeftRayX(nat,Le,?M)" by auto then have "⟨succ(?M),?M⟩∈Le" unfolding LeftRayX_def by blast then show "False" by auto qed subsection‹More Separation properties› text‹In this section we study more separation properties.› subsection‹Definitions› text‹We start with a property that has already appeared in @{file "Topology_ZF_1b.thy"}. A KC-space is a space where compact sets are closed.› definition IsKC ("_ {is KC}") where "T{is KC} ≡ ∀A∈Pow(⋃T). A{is compact in}T ⟶ A{is closed in}T" text‹Another type of space is an US-space; those where sequences have at most one limit.› definition IsUS ("_{is US}") where "T{is US} ≡ ∀N x y. (N:nat→⋃T) ∧ NetConvTop(⟨N,Le⟩,x,T) ∧ NetConvTop(⟨N,Le⟩,y,T) ⟶ y=x" subsection‹First results› text‹The proof in @{file "Topology_ZF_1b.thy"} shows that a Hausdorff space is KC.› corollary(in topology0) T2_imp_KC: assumes "T{is T⇩_{2}}" shows "T{is KC}" proof- { fix A assume "A{is compact in}T" then have "A{is closed in}T" using in_t2_compact_is_cl assms by auto } then show ?thesis unfolding IsKC_def by auto qed text‹From the spectrum of compactness, it follows that any KC-space is $T_1$.› lemma(in topology0) KC_imp_T1: assumes "T{is KC}" shows "T{is T⇩_{1}}" proof- { fix x assume A:"x∈⋃T" have "Finite({x})" by auto then have "{x}{is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto moreover have "(T{restricted to}{x}){is a topology}" using Top_1_L4 by auto moreover have "⋃(T{restricted to}{x})={x}" using A unfolding RestrictedTo_def by auto ultimately have com:"{x}{is compact in}(T{restricted to}{x})" unfolding Spec_def by auto then have "{x}{is compact in}T" using compact_subspace_imp_compact A by auto then have "{x}{is closed in}T" using assms unfolding IsKC_def using A by auto } then show ?thesis using T1_iff_singleton_closed by auto qed text‹Even more, if a space is KC, then it is US. We already know that for $T_2$ spaces, any net or filter has at most one limit; and that this property is equivalent with $T_2$. The US property is much weaker because we don't know what happends with other nets that are not directed by the order on the natural numbers.› theorem(in topology0) KC_imp_US: assumes "T{is KC}" shows "T{is US}" proof- { fix N x y assume A:"N:nat→⋃T" "⟨N,Le⟩→⇩_{N}x" "⟨N,Le⟩→⇩_{N}y" "x≠y" have dir:"Le directs nat" using Le_directs_nat by auto moreover from A(1) have dom:"domain(N)=nat" using func1_1_L1 by auto moreover note A(1) ultimately have Net:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def by auto from A(3) have y:"y∈⋃T" unfolding NetConverges_def[OF Net] by auto from A(2) have x:"x∈⋃T" unfolding NetConverges_def[OF Net] by auto from A(2) have o1:"∀U∈Pow(⋃T). x∈int(U) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" unfolding NetConverges_def[OF Net] using dom by auto { assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y" have "{y}{is closed in}T" using y T1_iff_singleton_closed KC_imp_T1 assms by auto then have o2:"⋃T-{y}∈T" unfolding IsClosed_def by auto then have "int(⋃T-{y})=⋃T-{y}" using Top_2_L3 by auto with A(4) x have o3:"x∈int(⋃T-{y})" by auto from o2 have "⋃T-{y}∈Pow(⋃T)" by auto with o1 o3 obtain r where r:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-{y}" by auto from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y" by auto from dir r(1) n(1) obtain z where "⟨r,z⟩∈Le""⟨n,z⟩∈Le""z∈nat" unfolding IsDirectedSet_def by auto with r(2) n(2) have "N`z∈⋃T-{y}" "N`z=y" by auto then have "False" by auto } then have reg:"∀n∈nat. ∃m∈nat. N`m≠y ∧ ⟨n,m⟩∈Le" by auto let ?NN="{⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩. n∈nat}" { fix x z assume A1:"⟨x, z⟩ ∈ ?NN" { fix y' assume A2:"⟨x,y'⟩∈?NN" with A1 have "z=y'" by auto } then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto } then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto moreover { fix n assume as:"n∈nat" with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"] nat_into_Ord[of "m"] by auto then have "(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈nat" by auto then have "N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈⋃T" using apply_type[OF A(1)] by auto with as have "⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃T" by auto } then have "?NN∈Pow(nat×⋃T)" by auto ultimately have NFun:"?NN:nat→⋃T" unfolding Pi_def function_def domain_def by auto { fix n assume as:"n∈nat" with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"] nat_into_Ord[of "m"] by auto then have "?NN`n≠y" using apply_equality[OF _ NFun] by auto } then have noy:"∀n∈nat. ?NN`n≠y" by auto have dom2:"domain(?NN)=nat" by auto then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using NFun dir by auto { fix U assume "U∈Pow(⋃T)" "x∈int(U)" then have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" using o1 by auto then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" by auto { fix s assume AA:"⟨r,s⟩∈Le" with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"] nat_into_Ord by auto with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈U" by blast then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto } then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto } then have conv2:"⟨?NN,Le⟩→⇩_{N}x" unfolding NetConverges_def[OF net2] using x dom2 by auto let ?A="{x}∪?NN``nat" { fix M assume Acov:"?A⊆⋃M" "M⊆T" then have "x∈⋃M" by auto then obtain U where U:"x∈U" "U∈M" by auto with Acov(2) have UT:"U∈T" by auto then have "U=int(U)" using Top_2_L3 by auto with U(1) have "x∈int(U)" by auto with conv2 obtain r where rr:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" unfolding NetConverges_def[OF net2] using dom2 UT by auto have NresFun:"restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}):{n∈nat. ⟨n,r⟩∈Le}→⋃T" using restrict_fun [OF NFun, of "{n∈nat. ⟨n,r⟩∈Le}"] by auto then have "restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})∈surj({n∈nat. ⟨n,r⟩∈Le},range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})))" using fun_is_surj by auto moreover have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto then have "{n∈nat. ⟨n,r⟩∈Le}≲nat" using subset_imp_lepoll by auto ultimately have "range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}))≲{n∈nat. ⟨n,r⟩∈Le}" using surj_fun_inv_2 by auto moreover have "{n∈nat. ⟨n,0⟩∈Le}={0}" by auto then have "Finite({n∈nat. ⟨n,0⟩∈Le})" by auto moreover { fix j assume as:"j∈nat" "Finite({n∈nat. ⟨n,j⟩∈Le})" { fix t assume "t∈{n∈nat. ⟨n,succ(j)⟩∈Le}" then have "t∈nat" "⟨t,succ(j)⟩∈Le" by auto then have "t≤succ(j)" by auto then have "t⊆succ(j)" using le_imp_subset by auto then have "t⊆j ∪{j}" using succ_explained by auto then have "j∈t∨t⊆j" by auto then have "j∈t∨t≤j" using subset_imp_le ‹t∈nat› ‹j∈nat› nat_into_Ord by auto then have "j ∪{j}⊆t∨t≤j" using ‹t∈nat› ‹j∈nat› nat_into_Ord unfolding Ord_def Transset_def by auto then have "succ(j)⊆t∨t≤j" using succ_explained by auto with ‹t⊆succ(j)› have "t=succ(j)∨t≤j" by auto with ‹t∈nat› ‹j∈nat› have "t∈{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto } then have "{n∈nat. ⟨n,succ(j)⟩∈Le} ⊆{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto moreover have "Finite({n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)})" using as(2) Finite_cons by auto ultimately have "Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" using subset_Finite by auto } then have "∀j∈nat. Finite({n∈nat. ⟨n,j⟩∈Le}) ⟶ Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" by auto ultimately have "Finite(range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le})))" using lepoll_Finite[of "range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))" "{n ∈ nat . ⟨n, r⟩ ∈ Le}"] ind_on_nat[OF ‹r∈nat›, where P="λt. Finite({n∈nat. ⟨n,t⟩∈Le})"] by auto then have "Finite((restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using range_image_domain[OF NresFun] by auto then have "Finite(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using restrict_image by auto then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto moreover have "⋃(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})=⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}" unfolding RestrictedTo_def by auto moreover have "⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}=?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}" using func1_1_L6(2)[OF NFun] by blast moreover have "(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is a topology}" using Top_1_L4 by auto ultimately have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" unfolding Spec_def by force then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}T" using compact_subspace_imp_compact by auto moreover from Acov(1) have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃M" by auto moreover note Acov(2) ultimately obtain 𝔑 where 𝔑:"𝔑∈FinPow(M)" "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃𝔑" unfolding IsCompact_def by blast from 𝔑(1) have "𝔑 ∪{U}∈FinPow(M)" using U(2) unfolding FinPow_def by auto moreover { fix s assume s:"s∈?A" "s∉U" with U(1) have "s∈?NN``nat" by auto then have "s∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto then obtain n where n:"n∈nat" "s=?NN`n" by auto { assume "⟨r,n⟩∈Le" with rr have "?NN`n∈U" by auto with n(2) s(2) have "False" by auto } then have "⟨r,n⟩∉Le" by auto with rr(1) n(1) have "¬(r≤n)" by auto then have "n≤r" using Ord_linear_le[where thesis="⟨n,r⟩∈Le"] nat_into_Ord[OF rr(1)] nat_into_Ord[OF n(1)] by auto with rr(1) n(1) have "⟨n,r⟩∈Le" by auto with n(2) have "s∈{?NN`t. t∈{n∈nat. ⟨n,r⟩∈Le}}" by auto moreover have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto ultimately have "s∈?NN``{n∈nat. ⟨n,r⟩∈Le}" using func_imagedef[OF NFun] by auto with 𝔑(2) have "s∈⋃𝔑" by auto } then have "?A⊆⋃𝔑 ∪ U" by auto then have "?A⊆⋃(𝔑 ∪ {U})" by auto ultimately have "∃𝔑∈FinPow(M). ?A⊆⋃𝔑" by auto } then have "∀M∈Pow(T). ?A⊆⋃M ⟶ (∃𝔑∈FinPow(M). ?A⊆⋃𝔑)" by auto moreover have "?A⊆⋃T" using func1_1_L6(2)[OF NFun] x by blast ultimately have "?A{is compact in}T" unfolding IsCompact_def by auto with assms have "?A{is closed in}T" unfolding IsKC_def IsCompact_def by auto then have "⋃T-?A∈T" unfolding IsClosed_def by auto then have "⋃T-?A=int(⋃T-?A)" using Top_2_L3 by auto moreover { assume "y∈?A" with A(4) have "y∈?NN``nat" by auto then have "y∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto then obtain n where "n∈nat""?NN`n=y" by auto with noy have "False" by auto } with y have "y∈⋃T-?A" by force ultimately have "y∈int(⋃T-?A)" "⋃T-?A∈Pow(⋃T)" by auto moreover have "(∀U∈Pow(⋃T). y ∈ int(U) ⟶ (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U))" using A(3) dom unfolding NetConverges_def[OF Net] by auto ultimately have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T-?A" by blast then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-?A" by auto { fix s assume AA:"⟨r,s⟩∈Le" with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"] nat_into_Ord by auto with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈⋃T-?A" by force then have "?NN`s∈⋃T-?A" using apply_equality[OF _ NFun] AA by auto moreover have "?NN`s∈{?NN`t. t∈nat}" using AA by auto then have "?NN`s∈?NN``nat" using func_imagedef[OF NFun] by auto then have "?NN`s∈?A" by auto ultimately have "False" by auto } moreover have "r⊆succ(r)" using succ_explained by auto then have "r≤succ(r)" using subset_imp_le nat_into_Ord ‹r∈nat› nat_succI by auto then have "⟨r,succ(r)⟩∈Le" using ‹r∈nat› nat_succI by auto ultimately have "False" by auto } then have "∀N x y. (N:nat→⋃T) ∧ (⟨N, Le⟩ →⇩_{N}x {in} T) ∧ (⟨N, Le⟩ →⇩_{N}y {in} T) ⟶ x=y" by auto then show ?thesis unfolding IsUS_def by auto qed text‹US spaces are also $T_1$.› theorem (in topology0) US_imp_T1: assumes "T{is US}" shows "T{is T⇩_{1}}" proof- { fix x assume x:"x∈⋃T" then have "{x}⊆⋃T" by auto { fix y assume y:"y≠x" "y∈cl({x})" then have r:"∀U∈T. y∈U ⟶ x∈U" using cl_inter_neigh[OF ‹{x}⊆⋃T›] by auto let ?N="ConstantFunction(nat,x)" have fun:"?N:nat→⋃T" using x func1_3_L1 by auto then have dom:"domain(?N)=nat" using func1_1_L1 by auto with fun have Net:"⟨?N,Le⟩{is a net on}⋃T" using Le_directs_nat unfolding IsNet_def by auto { fix U assume "U∈Pow(⋃T)" "x∈int(U)" then have "x∈U" using Top_2_L1 by auto then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto } then have "⟨?N,Le⟩ →⇩_{N}x" unfolding NetConverges_def[OF Net] using x dom by auto moreover { fix U assume "U∈Pow(⋃T)" "y∈int(U)" then have "x∈int(U)" using r Top_2_L2 by auto then have "x∈U" using Top_2_L1 by auto then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto } then have "⟨?N,Le⟩ →⇩_{N}y" unfolding NetConverges_def[OF Net] using y(2) dom Top_3_L11(1)[OF ‹{x}⊆⋃T›] by auto ultimately have "x=y" using assms unfolding IsUS_def using fun by auto with y(1) have "False" by auto } then have "cl({x})⊆{x}" by auto then have "cl({x})={x}" using cl_contains_set[OF ‹{x}⊆⋃T›] by auto then have "{x}{is closed in}T" using Top_3_L8 x by auto } then show ?thesis using T1_iff_singleton_closed by auto qed subsection‹Counter-examples› text‹We need to find counter-examples that prove that this properties are new ones.› text‹We know that $T_2\Rightarrow loc.T_2\Rightarrow$ anti-hyperconnected $\Rightarrow T_1$ and $T_2\Rightarrow KC\Rightarrow US\Rightarrow T_1$. The question is: What is the relation between $KC$ or $US$ and, $loc.T_2$ or anti-hyperconnected?› text‹In the file @{file "Topology_ZF_properties_2.thy"} we built a topological space which is locally-$T_2$ but no $T_2$. It happends actually that this space is not even US given the appropiate topology ‹T›.› lemma (in topology0) locT2_not_US_1: assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩_{N}m) ∧ m∉N``nat" shows "∃N∈nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). (⟨N,Le⟩→⇩_{N}⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})) ∧ (⟨N,Le⟩→⇩_{N}m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" proof- from assms(3) obtain N where N:"N:nat→⋃T" "⟨N,Le⟩→⇩_{N}m" "m∉N``nat" by auto have "⋃T⊆⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top by auto with N(1) have fun:"N:nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using func1_1_L1B by auto then have dom:"domain(N)=nat" using func1_1_L1 by auto with fun have Net:"⟨N,Le⟩{is a net on}⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" unfolding IsNet_def using Le_directs_nat by auto from N(1) dom have Net2:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def using Le_directs_nat by auto from N(2) have R:"∀U∈Pow(⋃T). m∈int(U) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" unfolding NetConverges_def[OF Net2] using dom by auto { fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" "m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast then have "(⋃T)∩?I∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" unfolding RestrictedTo_def by blast then have "(⋃T)∩?I∈T" using open_subspace_double_point(1) assms(2) by auto moreover then have "int((⋃T)∩?I)=(⋃T)∩?I" using Top_2_L3 by auto with U(2) assms(2) have "m∈int((⋃T)∩?I)" unfolding IsClosed_def by auto moreover note R ultimately have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈(⋃T)∩?I" by blast then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" by blast then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1[of "T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}""U"] doble_point_top assms(2) unfolding topology0_def by auto } then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto moreover have tt:"topology0(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using doble_point_top[OF assms(2)] unfolding topology0_def. have "m∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top unfolding IsClosed_def by auto ultimately have con1:"(⟨N,Le⟩→⇩_{N}m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net] using dom by auto { fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" "⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast with U(2) mem_not_refl have "?I∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain V W where VW:"?I=(V-{m})∪{⋃T}∪W" "W∈T" "V∈T" "m∈V" by auto from VW(3,4) have "m∈int(V)" using Top_2_L3 by auto moreover have "V∈Pow(⋃T)" using VW(3) by auto moreover note R ultimately have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V" by blast moreover from N(3) have "∀s∈nat. N`s≠m" using func_imagedef[OF N(1)] by auto ultimately have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V-{m}" by blast then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" using VW(1) by auto then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1 assms(2) doble_point_top unfolding topology0_def by blast } then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). ⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto moreover have "⋃T∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top by auto ultimately have "(⟨N,Le⟩→⇩_{N}⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net] using dom by auto with con1 fun show ?thesis by auto qed corollary (in topology0) locT2_not_US_2: assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩_{N}m) ∧ m∉N``nat" shows "¬((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){is US})" proof- have "m≠⋃T" using assms(2) mem_not_refl unfolding IsClosed_def by auto then show ?thesis using locT2_not_US_1 assms unfolding IsUS_def by blast qed text‹In particular, we also know that a locally-$T_2$ space doesn't need to be KC; since KC$\Rightarrow$US. Also we know that anti-hyperconnected spaces don't need to be KC or US, since locally-$T_2\Rightarrow$anti-hyperconnected.› text‹Let's find a KC space that is not $T_2$, an US space which is not KC and a $T_1$ space which is not US.› text‹First, let's prove some lemmas about what relation is there between this properties under the influence of other ones. This will help us to find counter-examples.› text‹Anti-compactness ereases the differences between several properties.› lemma (in topology0) anticompact_KC_equiv_T1: assumes "T{is anti-compact}" shows "T{is KC}⟷T{is T⇩_{1}}" proof assume "T{is KC}" then show "T{is T⇩_{1}}" using KC_imp_T1 by auto next assume AS:"T{is T⇩_{1}}" { fix A assume A:"A{is compact in}T" "A∈Pow(⋃T)" then have "A{is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" using compact_imp_compact_subspace Compact_is_card_nat by auto moreover then have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto ultimately have "(⋃(T{restricted to}A)){is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" by auto with assms have "Finite(A)" unfolding IsAntiComp_def antiProperty_def using compact_spectrum by auto then obtain n where "n∈nat" "A≈n" unfolding Finite_def by auto then have "A≺nat" using eq_lesspoll_trans n_lesspoll_nat by auto moreover have "⋃T-(⋃T-A)=A" using A(2) by auto ultimately have "⋃T-(⋃T-A)≺nat" by auto then have "⋃T-A∈CoFinite ⋃T" unfolding Cofinite_def CoCardinal_def by auto then have "⋃T-A∈T" using AS T1_cocardinal_coarser by auto with A(2) have "A{is closed in}T" unfolding IsClosed_def by auto } then show "T{is KC}" unfolding IsKC_def by auto qed text‹Then if we find an anti-compact and $T_1$ but no $T_2$ space, there is a counter-example for $KC\Rightarrow T_2$. A counter-example for US doesn't need to be KC mustn't be anti-compact.› text‹The cocountable topology on ‹csucc(nat)› is such a topology.› text‹The cocountable topology on $\mathbb{N}^+$ is hyperconnected.› lemma cocountable_in_csucc_nat_HConn: shows "(CoCountable csucc(nat)){is hyperconnected}" proof- { fix U V assume as:"U∈(CoCountable csucc(nat))""V∈(CoCountable csucc(nat))""U∩V=0" then have "csucc(nat)-U≺csucc(nat)∨U=0""csucc(nat)-V≺csucc(nat)∨V=0" unfolding Cocountable_def CoCardinal_def by auto then have "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)∨U=0∨V=0" using less_less_imp_un_less[ OF _ _ InfCard_csucc[OF InfCard_nat]] by auto moreover { assume "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)" moreover have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)-U∩V" by auto with as(3) have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)" by auto ultimately have "csucc(nat)≺csucc(nat)" by auto then have "False" by auto } ultimately have "U=0∨V=0" by auto } then show "(CoCountable csucc(nat)){is hyperconnected}" unfolding IsHConnected_def by auto qed text‹The cocountable topology on $\mathbb{N}^+$ is not anti-hyperconnected.› corollary cocountable_in_csucc_nat_notAntiHConn: shows "¬((CoCountable csucc(nat)){is anti-}IsHConnected)" proof assume as:"(CoCountable csucc(nat)){is anti-}IsHConnected" have "(CoCountable csucc(nat)){is hyperconnected}" using cocountable_in_csucc_nat_HConn by auto moreover have "csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto then have uni:"⋃(CoCountable csucc(nat))=csucc(nat)" using union_cocardinal unfolding Cocountable_def by auto have "∀A∈(CoCountable csucc(nat)). A⊆⋃(CoCountable csucc(nat))" by fast with uni have "∀A∈(CoCountable csucc(nat)). A⊆csucc(nat)" by auto then have "∀A∈(CoCountable csucc(nat)). csucc(nat)∩A=A" by auto ultimately have "((CoCountable csucc(nat)){restricted to}csucc(nat)){is hyperconnected}" unfolding RestrictedTo_def by auto with as have "(csucc(nat)){is in the spectrum of}IsHConnected" unfolding antiProperty_def using uni by auto then have "csucc(nat)≲1" using HConn_spectrum by auto then have "csucc(nat)≺nat" using n_lesspoll_nat lesspoll_trans1 by auto then show "False" using lt_csucc[OF Ord_nat] lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lesspoll_trans by auto qed text‹The cocountable topology on $\mathbb{N}^+$ is not $T_2$.› theorem cocountable_in_csucc_nat_noT2: shows "¬(CoCountable csucc(nat)){is T⇩_{2}}" proof assume "(CoCountable csucc(nat)){is T⇩_{2}}" then have antiHC:"(CoCountable csucc(nat))