(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2012-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 ‹Topology 5› theory Topology_ZF_5 imports Topology_ZF_properties Topology_ZF_examples_1 Topology_ZF_4 begin subsection‹Some results for separation axioms› text‹First we will give a global characterization of $T_1$-spaces; which is interesting because it involves the cardinal $\mathbb{N}$.› lemma (in topology0) T1_cocardinal_coarser: shows "(T {is T⇩_{1}}) ⟷ (CoFinite (⋃T))⊆T" proof { assume AS:"T {is T⇩_{1}}" { fix x assume p:"x∈⋃T" { fix y assume "y∈(⋃T)-{x}" with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto } then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto then have "⋃T-{x}∈T" using open_neigh_open by auto with p have "{x} {is closed in}T" using IsClosed_def by auto } then have pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto { fix A assume AS2:"A∈FinPow(⋃T)" let ?p="{⟨x,{x}⟩. x∈A}" have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality by auto then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def by (safe, blast+) then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto moreover have "⋃{{x}. x∈A}=A" by auto ultimately have "A {is closed in} T" by simp } then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto { fix U assume AS2:"U ∈ CoCardinal(⋃T,nat)" then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum reg unfolding FinPow_def by auto then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto moreover then have "(⋃T-(⋃T-U))=U" by blast ultimately have "U∈T" by auto } then show "(CoFinite (⋃T))⊆T" using Cofinite_def by auto } { assume "(CoFinite (⋃T))⊆T" then have AS:"CoCardinal(⋃T,nat) ⊆ T" using Cofinite_def by auto { fix x y assume AS2:"x∈⋃T" "y∈⋃T""x≠y" have "Finite({y})" by auto then obtain n where "{y}≈n" "n∈nat" using Finite_def by auto then have "{y}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto then have "{y} {is closed in} CoCardinal(⋃T,nat)" using closed_sets_cocardinal AS2(2) by auto then have "(⋃T)-{y}∈CoCardinal(⋃T,nat)" using union_cocardinal IsClosed_def by auto with AS have "(⋃T)-{y}∈T" by auto moreover with AS2(1,3) have "x∈((⋃T)-{y}) ∧ y∉((⋃T)-{y})" by auto ultimately have "∃V∈T. x∈V∧y∉V" by(safe,auto) } then show "T {is T⇩_{1}}" using isT1_def by auto } qed text‹In the previous proof, it is obvious that we don't need to check if ever cofinite set is open. It is enough to check if every singleton is closed.› corollary(in topology0) T1_iff_singleton_closed: shows "(T {is T⇩_{1}}) ⟷ (∀x∈⋃T. {x}{is closed in}T)" proof assume AS:"T {is T⇩_{1}}" { fix x assume p:"x∈⋃T" { fix y assume "y∈(⋃T)-{x}" with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto } then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto then have "⋃T-{x}∈T" using open_neigh_open by auto with p have "{x} {is closed in}T" using IsClosed_def by auto } then show pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto next assume pointCl:"∀x∈⋃T. {x} {is closed in} T" { fix A assume AS2:"A∈FinPow(⋃T)" let ?p="{⟨x,{x}⟩. x∈A}" have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality by auto then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def by (safe, blast+) then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto moreover have "⋃{{x}. x∈A}=A" by auto ultimately have "A {is closed in} T" by simp } then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto { fix U assume AS2:"U∈CoCardinal(⋃T,nat)" then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum reg unfolding FinPow_def by auto then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto moreover then have "(⋃T-(⋃T-U))=U" by blast ultimately have "U∈T" by auto } then have "(CoFinite (⋃T))⊆T" using Cofinite_def by auto then show "T {is T⇩_{1}}" using T1_cocardinal_coarser by auto qed text‹Secondly, let's show that the ‹CoCardinal X Q› topologies for different sets $Q$ are all ordered as the partial order of sets. (The order is linear when considering only cardinals)› lemma order_cocardinal_top: fixes X assumes "Q1≲Q2" shows "CoCardinal(X,Q1) ⊆ CoCardinal(X,Q2)" proof fix x assume "x ∈ CoCardinal(X,Q1)" then have "x∈Pow(X)" "x=0∨(X-x)≺Q1" using CoCardinal_def by auto with assms have "x∈Pow(X)" "x=0∨(X-x)≺Q2" using lesspoll_trans2 by auto then show "x∈CoCardinal(X,Q2)" using CoCardinal_def by auto qed corollary cocardinal_is_T1: fixes X K assumes "InfCard(K)" shows "CoCardinal(X,K) {is T⇩_{1}}" proof- have "nat≤K" using InfCard_def assms by auto then have "nat⊆K" using le_imp_subset by auto then have "nat≲K" "K≠0"using subset_imp_lepoll by auto then have "CoCardinal(X,nat) ⊆ CoCardinal(X,K)" "⋃CoCardinal(X,K)=X" using order_cocardinal_top union_cocardinal by auto then show ?thesis using topology0.T1_cocardinal_coarser topology0_CoCardinal assms Cofinite_def by auto qed text‹In $T_2$-spaces, filters and nets have at most one limit point.› lemma (in topology0) T2_imp_unique_limit_filter: assumes "T {is T⇩_{2}}" "𝔉 {is a filter on}⋃T" "𝔉 →⇩_{F}x" "𝔉 →⇩_{F}y" shows "x=y" proof- { assume "x≠y" from assms(3,4) have "x∈⋃T" "y∈⋃T" using FilterConverges_def assms(2) by auto with ‹x≠y› have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" using assms(1) isT2_def by auto then obtain U V where "x∈U" "y∈V" "U∩V=0" "U∈T" "V∈T" by auto then have "U∈{A∈Pow(⋃T). x∈Interior(A,T)}" "V∈{A∈Pow(⋃T). y∈Interior(A,T)}" using Top_2_L3 by auto then have "U∈𝔉" "V∈𝔉" using FilterConverges_def assms(2) assms(3,4) by auto then have "U∩V∈𝔉" using IsFilter_def assms(2) by auto with ‹U∩V=0› have "0∈𝔉" by auto then have "False" using IsFilter_def assms(2) by auto } then show ?thesis by auto qed lemma (in topology0) T2_imp_unique_limit_net: assumes "T {is T⇩_{2}}" "N {is a net on}⋃T" "N →⇩_{N}x" "N →⇩_{N}y" shows "x=y" proof- have "(Filter N..(⋃T)) {is a filter on} (⋃T)" "(Filter N..(⋃T)) →⇩_{F}x" "(Filter N..(⋃T)) →⇩_{F}y" using filter_of_net_is_filter(1) net_conver_filter_of_net_conver assms(2) assms(3,4) by auto with assms(1) show ?thesis using T2_imp_unique_limit_filter by auto qed text‹In fact, $T_2$-spaces are characterized by this property. For this proof we build a filter containing the union of two filters.› lemma (in topology0) unique_limit_filter_imp_T2: assumes "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩_{F}x) ∧ (𝔉 →⇩_{F}y)) ⟶ x=y" shows "T {is T⇩_{2}}" proof- { fix x y assume "x∈⋃T" "y∈⋃T" "x≠y" { assume "∀U∈T. ∀V∈T. (x∈U ∧ y∈V) ⟶ U∩V≠0" let ?Ux="{A∈Pow(⋃T). x∈int(A)}" let ?Uy="{A∈Pow(⋃T). y∈int(A)}" let ?FF="?Ux ∪ ?Uy ∪ {A∩B. ⟨A,B⟩∈?Ux × ?Uy}" have sat:"?FF {satisfies the filter base condition}" proof- { fix A B assume "A∈?FF" "B∈?FF" { assume "A∈?Ux" { assume "B∈?Ux" with ‹x∈⋃T› ‹A∈?Ux› have "A∩B∈?Ux" using neigh_filter(1) IsFilter_def by auto then have "A∩B∈?FF" by auto } moreover { assume "B∈?Uy" with ‹A∈?Ux› have "A∩B∈?FF" by auto } moreover { assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto with ‹x∈⋃T› ‹A∈?Ux› have "A∩B=(A∩AA)∩BB" "A∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto with ‹BB∈?Uy› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto then have "A∩B∈?FF" by auto } ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto } moreover { assume "A∈?Uy" { assume "B∈?Uy" with ‹y∈⋃T› ‹A∈?Uy› have "A∩B∈?Uy" using neigh_filter(1) IsFilter_def by auto then have "A∩B∈?FF" by auto } moreover { assume "B∈?Ux" with ‹A∈?Uy› have "B∩A∈?FF" by auto moreover have "A∩B=B∩A" by auto ultimately have "A∩B∈?FF" by auto } moreover { assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto with ‹y∈⋃T› ‹A∈?Uy› have "A∩B=AA∩(A∩BB)" "A∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto with ‹AA∈?Ux› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto then have "A∩B∈?FF" by auto } ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto } moreover { assume "A∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" then obtain AA BB where "A=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto { assume "B∈?Uy" with ‹BB∈?Uy› ‹y∈⋃T› have "B∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto moreover from ‹A=AA∩BB› have "A∩B=AA∩(B∩BB)" by auto ultimately have "A∩B∈?FF" using ‹AA∈?Ux› ‹B∩BB∈?Uy› by auto } moreover { assume "B∈?Ux" with ‹AA∈?Ux› ‹x∈⋃T› have "B∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto moreover from ‹A=AA∩BB› have "A∩B=(B∩AA)∩BB" by auto ultimately have "A∩B∈?FF" using ‹B∩AA∈?Ux› ‹BB∈?Uy› by auto } moreover { assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" then obtain AA2 BB2 where "B=AA2∩BB2" "AA2∈?Ux" "BB2∈?Uy" by auto from ‹B=AA2∩BB2› ‹A=AA∩BB› have "A∩B=(AA∩AA2)∩(BB∩BB2)" by auto moreover from ‹AA∈?Ux›‹AA2∈?Ux›‹x∈⋃T› have "AA∩AA2∈?Ux" using neigh_filter(1) IsFilter_def by auto moreover from ‹BB∈?Uy›‹BB2∈?Uy›‹y∈⋃T› have "BB∩BB2∈?Uy" using neigh_filter(1) IsFilter_def by auto ultimately have "A∩B∈?FF" by auto } ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto } ultimately have "A∩B∈?FF" using ‹A∈?FF› by auto then have "∃D∈?FF. D⊆A∩B" unfolding Bex_def by auto } then have "∀A∈?FF. ∀B∈?FF. ∃D∈?FF. D⊆A∩B" by force moreover have "⋃T∈?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto then have "?FF≠0" by auto moreover { assume "0∈?FF" moreover have "0∉?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto moreover have "0∉?Uy" using ‹y∈⋃T› neigh_filter(1) IsFilter_def by auto ultimately have "0∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto then obtain A B where "0=A∩B" "A∈?Ux""B∈?Uy" by auto then have "x∈int(A)""y∈int(B)" by auto moreover with ‹0=A∩B› have "int(A)∩int(B)=0" using Top_2_L1 by auto moreover have "int(A)∈T""int(B)∈T" using Top_2_L2 by auto ultimately have "False" using ‹∀U∈T. ∀V∈T. x∈U∧y∈V ⟶ U∩V≠0› by auto } then have "0∉?FF" by auto ultimately show ?thesis using SatisfiesFilterBase_def by auto qed moreover have "?FF⊆Pow(⋃T)" by auto ultimately have bas:"?FF {is a base filter} {A∈Pow(⋃T). ∃D∈?FF. D⊆A}" "⋃{A∈Pow(⋃T). ∃D∈?FF. D⊆A}=⋃T" using base_unique_filter_set2[of "?FF"] by auto then have fil:"{A∈Pow(⋃T). ∃D∈?FF. D⊆A} {is a filter on} ⋃T" using basic_filter sat by auto have "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩_{F}x" using convergence_filter_base2[OF fil bas(1) _ ‹x∈⋃T›] by auto moreover then have "∀U∈Pow(⋃T). y∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩_{F}y" using convergence_filter_base2[OF fil bas(1) _ ‹y∈⋃T›] by auto ultimately have "x=y" using assms fil ‹x∈⋃T›‹y∈⋃T› by blast with ‹x≠y› have "False" by auto } then have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" by blast } then show ?thesis using isT2_def by auto qed lemma (in topology0) unique_limit_net_imp_T2: assumes "∀x∈⋃T. ∀y∈⋃T. ∀N. ((N {is a net on}⋃T) ∧ (N →⇩_{N}x) ∧ (N →⇩_{N}y)) ⟶ x=y" shows "T {is T⇩_{2}}" proof- { fix x y 𝔉 assume "x∈⋃T" "y∈⋃T""𝔉 {is a filter on}⋃T""𝔉 →⇩_{F}x""𝔉 →⇩_{F}y" then have "(Net(𝔉)) {is a net on} ⋃T""(Net 𝔉) →⇩_{N}x""(Net 𝔉) →⇩_{N}y" using filter_conver_net_of_filter_conver net_of_filter_is_net by auto with ‹x∈⋃T› ‹y∈⋃T› have "x=y" using assms by blast } then have "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩_{F}x) ∧ (𝔉 →⇩_{F}y)) ⟶ x=y" by auto then show ?thesis using unique_limit_filter_imp_T2 by auto qed text‹This results make easy to check if a space is $T_2$.› text‹The topology which comes from a filter as in @{thm "top_of_filter"} is not $T_2$ generally. We will see in this file later on, that the exceptions are a consequence of the spectrum.› corollary filter_T2_imp_card1: assumes "(𝔉∪{0}) {is T⇩_{2}}" "𝔉 {is a filter on} ⋃𝔉" "x∈⋃𝔉" shows "⋃𝔉={x}" proof- { fix y assume "y∈⋃𝔉" then have "𝔉 →⇩_{F}y {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2) by auto moreover have "𝔉 →⇩_{F}x {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2,3) by auto moreover have "⋃𝔉=⋃(𝔉∪{0})" by auto ultimately have "y=x" using topology0.T2_imp_unique_limit_filter[OF topology0_filter[OF assms(2)] assms(1)] assms(2) by auto } then have "⋃𝔉⊆{x}" by auto with assms(3) show ?thesis by auto qed text‹There are more separation axioms that just $T_0$, $T_1$ or $T_2$› definition isT3 ("_{is T⇩_{3}}" 90) where "T{is T⇩_{3}} ≡ (T{is T⇩_{1}}) ∧ (T{is regular})" definition IsNormal ("_{is normal}" 90) where "T{is normal} ≡ ∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶ (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))" definition isT4 ("_{is T⇩_{4}}" 90) where "T{is T⇩_{4}} ≡ (T{is T⇩_{1}}) ∧ (T{is normal})" lemma (in topology0) T4_is_T3: assumes "T{is T⇩_{4}}" shows "T{is T⇩_{3}}" proof- from assms have nor:"T{is normal}" using isT4_def by auto from assms have "T{is T⇩_{1}}" using isT4_def by auto then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto { fix A assume AS:"A{is closed in}T" { fix x assume "x∈⋃T-A" have "Finite({x})" by auto then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto with ‹x∈⋃T-A› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def closed_sets_cocardinal by auto then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def by auto with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto with ‹x∈⋃T-A› have "{x}{is closed in}T" "A∩{x}=0" using IsClosed_def by auto with nor AS have "∃U∈T. ∃V∈T. A⊆U∧{x}⊆V∧U∩V=0" unfolding IsNormal_def by blast then have "∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto } then have "∀x∈⋃T-A. ∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto } then have "T{is regular}" using IsRegular_def by blast with ‹T{is T⇩_{1}}› show ?thesis using isT3_def by auto qed lemma (in topology0) T3_is_T2: assumes "T{is T⇩_{3}}" shows "T{is T⇩_{2}}" proof- from assms have "T{is regular}" using isT3_def by auto from assms have "T{is T⇩_{1}}" using isT3_def by auto then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto { fix x y assume "x∈⋃T""y∈⋃T""x≠y" have "Finite({x})" by auto then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto with ‹x∈⋃T› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def closed_sets_cocardinal by auto then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def by auto with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto with ‹x∈⋃T›‹y∈⋃T›‹x≠y› have "{x}{is closed in}T" "y∈⋃T-{x}" using IsClosed_def by auto with ‹T{is regular}› have "∃U∈T. ∃V∈T. {x}⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by force then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" by auto } then show ?thesis using isT2_def by auto qed text‹Regularity can be rewritten in terms of existence of certain neighboorhoods.› lemma (in topology0) regular_imp_exist_clos_neig: assumes "T{is regular}" and "U∈T" and "x∈U" shows "∃V∈T. x∈V ∧ cl(V)⊆U" proof- from assms(2) have "(⋃T-U){is closed in}T" using Top_3_L9 by auto moreover from assms(2,3) have "x∈⋃T" by auto moreover note assms(1,3) ultimately obtain A B where "A∈T" and "B∈T" and "A∩B=0" and "(⋃T-U)⊆A" and "x∈B" unfolding IsRegular_def by blast from ‹A∩B=0› ‹B∈T› have "B⊆⋃T-A" by auto with ‹A∈T› have "cl(B)⊆⋃T-A" using Top_3_L9 Top_3_L13 by auto moreover from ‹(⋃T-U)⊆A› assms(3) have "⋃T-A⊆U" by auto moreover note ‹x∈B› ‹B∈T› ultimately have "B∈T ∧ x∈B ∧ cl(B)⊆U" by auto then show ?thesis by auto qed lemma (in topology0) exist_clos_neig_imp_regular: assumes "∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U)" shows "T{is regular}" proof- { fix F assume "F{is closed in}T" { fix x assume "x∈⋃T-F" with ‹F{is closed in}T› have "x∈⋃T" "⋃T-F∈T" "F⊆⋃T" unfolding IsClosed_def by auto with assms ‹x∈⋃T-F› have "∃V∈T. x∈V ∧ cl(V)⊆⋃T-F" by auto then obtain V where "V∈T" "x∈V" "cl(V)⊆⋃T-F" by auto from ‹cl(V)⊆⋃T-F› ‹F⊆⋃T› have "F⊆⋃T-cl(V)" by auto moreover from ‹V∈T› have "⋃T-(⋃T-V)=V" by auto then have "cl(V)=⋃T-int(⋃T-V)" using Top_3_L11(2)[of "⋃T-V"] by auto ultimately have "F⊆int(⋃T-V)" by auto moreover have "int(⋃T-V)⊆⋃T-V" using Top_2_L1 by auto then have "V∩(int(⋃T-V))=0" by auto moreover note ‹x∈V›‹V∈T› ultimately have "V∈T" "int(⋃T-V)∈T" "F⊆int(⋃T-V) ∧ x∈V ∧ (int(⋃T-V))∩V=0" using Top_2_L2 by auto then have "∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto } then have "∀x∈⋃T-F. ∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto } then show ?thesis using IsRegular_def by blast qed lemma (in topology0) regular_eq: shows "T{is regular} ⟷ (∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U))" using regular_imp_exist_clos_neig exist_clos_neig_imp_regular by force text‹A Hausdorff space separates compact spaces from points.› theorem (in topology0) T2_compact_point: assumes "T{is T⇩_{2}}" "A{is compact in}T" "x∈⋃T" "x∉A" shows "∃U∈T. ∃V∈T. A⊆U ∧ x∈V ∧ U∩V=0" proof- { assume "A=0" then have "A⊆0∧x∈⋃T∧(0∩(⋃T)=0)" using assms(3) by auto then have ?thesis using empty_open topSpaceAssum unfolding IsATopology_def by auto } moreover { assume noEmpty:"A≠0" let ?U="{⟨U,V⟩∈T×T. x∈U∧U∩V=0}" { fix y assume "y∈A" with ‹x∉A› assms(4) have "x≠y" by auto moreover from ‹y∈A› have "x∈⋃T""y∈⋃T" using assms(2,3) unfolding IsCompact_def by auto ultimately obtain U V where "U∈T""V∈T""U∩V=0""x∈U""y∈V" using assms(1) unfolding isT2_def by blast then have "∃⟨U,V⟩∈?U. y∈V" by auto } then have "∀y∈A. ∃⟨U,V⟩∈?U. y∈V" by auto then have "A⊆⋃{snd(B). B∈?U}" by auto moreover have "{snd(B). B∈?U}∈Pow(T)" by auto ultimately have "∃N∈FinPow({snd(B). B∈?U}). A⊆⋃N" using assms(2) unfolding IsCompact_def by auto then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "A⊆⋃N" by auto with ‹{snd(B). B∈?U}∈Pow(T)› have "A⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto then have NN:"A⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def by auto then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto then have "N≲n" using eqpoll_imp_lepoll by auto from noEmpty ‹A⊆⋃N› have NnoEmpty:"N≠0" by auto let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}" have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto { fix n assume "n∈N" with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto ultimately have "?QQ`n≠0" by auto } then have "∀n∈N. ?QQ`n≠0" by auto with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def by auto then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast) { fix t assume "t∈N" then have "f`t∈?QQ`t" using fPI(2) by auto with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto } then have reg:"∀t∈N. f`t∈⋃(?QQ``N)" "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto { fix tt assume "tt∈f" with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto with reg(2) have "y∈⋃(?QQ``N)" by blast with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto } then have ffun:"f:N→⋃(?QQ``N)" using fPI(1) unfolding Pi_def by auto then have "f∈surj(N,range(f))" using fun_is_surj by auto with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto then have "range(f)⊆T" by auto ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover { fix S assume "S∈range(f)" with rr have "S∈⋃(?QQ``N)" by blast then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto then obtain B where "B∈(?QQ``N)" "S∈B" by auto then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto then have "x∈S" by auto } then have "x∈⋂range(f)" using ‹range(f)≠0› by auto moreover { fix y assume "y∈(⋃N)∩(⋂range(f))" then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto then obtain t where "t∈N" "y∈t" by auto then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto then have "f`t∈range(f)" using apply_rangeI ffun by auto with reg have yft:"y∈f`t" by auto with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto then have "⟨f`t,t⟩∈?U" by auto then have "f`t∩t=0" by auto with ‹y∈t› yft have "False" by auto } then have "(⋃N)∩(⋂range(f))=0" by blast moreover note NN ultimately have ?thesis by auto } ultimately show ?thesis by auto qed text‹A Hausdorff space separates compact spaces from other compact spaces.› theorem (in topology0) T2_compact_compact: assumes "T{is T⇩_{2}}" "A{is compact in}T" "B{is compact in}T" "A∩B=0" shows "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0" proof- { assume "B=0" then have "A⊆⋃T∧B⊆0∧((⋃T)∩0=0)" using assms(2) unfolding IsCompact_def by auto moreover have "0∈T" using empty_open topSpaceAssum by auto moreover have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have ?thesis by auto } moreover { assume noEmpty:"B≠0" let ?U="{⟨U,V⟩∈T×T. A⊆U ∧ U∩V=0}" { fix y assume "y∈B" then have "y∈⋃T" using assms(3) unfolding IsCompact_def by auto with ‹y∈B› have "∃U∈T. ∃V∈T. A⊆U ∧ y∈V ∧ U∩V=0" using T2_compact_point assms(1,2,4) by auto then have "∃⟨U,V⟩∈?U. y∈V" by auto } then have "∀y∈B. ∃⟨U,V⟩∈?U. y∈V" by auto then have "B⊆⋃{snd(B). B∈?U}" by auto moreover have "{snd(B). B∈?U}∈Pow(T)" by auto ultimately have "∃N∈FinPow({snd(B). B∈?U}). B⊆⋃N" using assms(3) unfolding IsCompact_def by auto then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "B⊆⋃N" by auto with ‹{snd(B). B∈?U}∈Pow(T)› have "B⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto then have NN:"B⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def by auto then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto then have "N≲n" using eqpoll_imp_lepoll by auto from noEmpty ‹B⊆⋃N› have NnoEmpty:"N≠0" by auto let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}" have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto { fix n assume "n∈N" with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto ultimately have "?QQ`n≠0" by auto } then have "∀n∈N. ?QQ`n≠0" by auto with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def by auto then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast) { fix t assume "t∈N" then have "f`t∈?QQ`t" using fPI(2) by auto with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto } then have reg:"∀t∈N. f`t∈⋃(?QQ``N)" "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto { fix tt assume "tt∈f" with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto with reg(2) have "y∈⋃(?QQ``N)" by blast with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto } then have ffun:"f:N→⋃(?QQ``N)" using fPI(1) unfolding Pi_def by auto then have "f∈surj(N,range(f))" using fun_is_surj by auto with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto then have "range(f)⊆T" by auto ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover { fix S assume "S∈range(f)" with rr have "S∈⋃(?QQ``N)" by blast then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto then obtain B where "B∈(?QQ``N)" "S∈B" by auto then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto then have "A⊆S" by auto } then have "A⊆⋂range(f)" using ‹range(f)≠0› by auto moreover { fix y assume "y∈(⋃N)∩(⋂range(f))" then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto then obtain t where "t∈N" "y∈t" by auto then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto then have "f`t∈range(f)" using apply_rangeI ffun by auto with reg have yft:"y∈f`t" by auto with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto then have "⟨f`t,t⟩∈?U" by auto then have "f`t∩t=0" by auto with ‹y∈t› yft have "False" by auto } then have "(⋂range(f))∩(⋃N)=0" by blast moreover note NN ultimately have ?thesis by auto } ultimately show ?thesis by auto qed text‹A compact Hausdorff space is normal.› corollary (in topology0) T2_compact_is_normal: assumes "T{is T⇩_{2}}" "(⋃T){is compact in}T" shows "T{is normal}" unfolding IsNormal_def proof- from assms(2) have car_nat:"(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto { fix A B assume "A{is closed in}T" "B{is closed in}T""A∩B=0" then have com:"((⋃T)∩A){is compact of cardinal}nat{in}T" "((⋃T)∩B){is compact of cardinal}nat{in}T" using compact_closed[OF car_nat] by auto from ‹A{is closed in}T›‹B{is closed in}T› have "(⋃T)∩A=A""(⋃T)∩B=B" unfolding IsClosed_def by auto with com have "A{is compact of cardinal}nat{in}T" "B{is compact of cardinal}nat{in}T" by auto then have "A{is compact in}T""B{is compact in}T" using Compact_is_card_nat by auto with ‹A∩B=0› have "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0" using T2_compact_compact assms(1) by auto } then show " ∀A. A {is closed in} T ⟶ (∀B. B {is closed in} T ∧ A ∩ B = 0 ⟶ (∃U∈T. ∃V∈T. A ⊆ U ∧ B ⊆ V ∧ U ∩ V = 0))" by auto qed subsection‹Hereditability› text‹A topological property is hereditary if whenever a space has it, every subspace also has it.› definition IsHer ("_{is hereditary}" 90) where "P {is hereditary} ≡ ∀T. T{is a topology} ∧ P(T) ⟶ (∀A∈Pow(⋃T). P(T{restricted to}A))" lemma subspace_of_subspace: assumes "A⊆B""B⊆⋃T" shows "T{restricted to}A=(T{restricted to}B){restricted to}A" proof from assms have S:"∀S∈T. A∩(B∩S)=A∩S" by auto then show "T {restricted to} A ⊆ T {restricted to} B {restricted to} A" unfolding RestrictedTo_def by auto from S show "T {restricted to} B {restricted to} A ⊆ T {restricted to} A" unfolding RestrictedTo_def by auto qed text‹The separation properties $T_0$, $T_1$, $T_2$ y $T_3$ are hereditary.› theorem regular_here: assumes "T{is regular}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is regular}" proof- { fix C assume A:"C{is closed in}(T{restricted to}A)" {fix y assume "y∈⋃(T{restricted to}A)""y∉C" with A have "(⋃(T{restricted to}A))-C∈(T{restricted to}A)""C⊆⋃(T{restricted to}A)" "y∈⋃(T{restricted to}A)""y∉C" unfolding IsClosed_def by auto moreover with assms(2) have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto ultimately have "A-C∈T{restricted to}A" "y∈A""y∉C""C∈Pow(A)" by auto then obtain S where "S∈T" "A∩S=A-C" "y∈A""y∉C" unfolding RestrictedTo_def by auto then have "y∈A-C""A∩S=A-C" by auto with ‹C∈Pow(A)› have "y∈A∩S""C=A-A∩S" by auto then have "y∈S" "C=A-S" by auto with assms(2) have "y∈S" "C⊆⋃T-S" by auto moreover from ‹S∈T› have "⋃T-(⋃T-S)=S" by auto moreover with ‹S∈T› have "(⋃T-S) {is closed in}T" using IsClosed_def by auto ultimately have "y∈⋃T-(⋃T-S)" "(⋃T-S) {is closed in}T" by auto with assms(1) have "∀y∈⋃T-(⋃T-S). ∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by auto with ‹y∈⋃T-(⋃T-S)› have "∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" by auto then obtain U V where "U∈T""V∈T" "⋃T-S⊆U""y∈V""U∩V=0" by auto then have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "C⊆U""y∈V""(A∩U)∩(A∩V)=0" unfolding RestrictedTo_def using ‹C⊆⋃T-S› by auto moreover with ‹C∈Pow(A)›‹y∈A› have "C⊆A∩U""y∈A∩V" by auto ultimately have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧y∈V∧U∩V=0" by auto } then have "∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0" by auto } then have "∀C. C{is closed in}(T{restricted to}A) ⟶ (∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0)" by blast then show ?thesis using IsRegular_def by auto qed corollary here_regular: shows "IsRegular {is hereditary}" using regular_here IsHer_def by auto theorem T1_here: assumes "T{is T⇩_{1}}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩_{1}}" proof- from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto { fix x y assume "x∈A""y∈A""x≠y" with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto then have "∃U∈T. x∈U∧y∉U" using assms(1) isT1_def by auto then obtain U where "U∈T""x∈U""y∉U" by auto with ‹x∈A› have "A∩U∈(T{restricted to}A)" "x∈A∩U" "y∉A∩U" unfolding RestrictedTo_def by auto then have "∃U∈(T{restricted to}A). x∈U∧y∉U" by blast } with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). x∈U∧y∉U)" by auto then show ?thesis using isT1_def by auto qed corollary here_T1: shows "isT1 {is hereditary}" using T1_here IsHer_def by auto lemma here_and: assumes "P {is hereditary}" "Q {is hereditary}" shows "(λT. P(T) ∧ Q(T)) {is hereditary}" using assms unfolding IsHer_def by auto corollary here_T3: shows "isT3 {is hereditary}" using here_and[OF here_T1 here_regular] unfolding IsHer_def isT3_def. lemma T2_here: assumes "T{is T⇩_{2}}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩_{2}}" proof- from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto { fix x y assume "x∈A""y∈A""x≠y" with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(1) isT2_def by auto then obtain U V where "U∈T" "V∈T""x∈U""y∈V""U∩V=0" by auto with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "x∈A∩U" "y∈A∩V" "(A∩U)∩(A∩V)=0"unfolding RestrictedTo_def by auto then have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0" unfolding Bex_def by auto } with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0)" by auto then show ?thesis using isT2_def by auto qed corollary here_T2: shows "isT2 {is hereditary}" using T2_here IsHer_def by auto lemma T0_here: assumes "T{is T⇩_{0}}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩_{0}}" proof- from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto { fix x y assume "x∈A""y∈A""x≠y" with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto then have "∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U)" using assms(1) isT0_def by auto then obtain U where "U∈T" "(x∈U∧y∉U)∨(y∈U∧x∉U)" by auto with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)" "(x∈A∩U∧y∉A∩U)∨(y∈A∩U∧x∉A∩U)" unfolding RestrictedTo_def by auto then have "∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U)" unfolding Bex_def by auto } with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U))" by auto then show ?thesis using isT0_def by auto qed corollary here_T0: shows "isT0 {is hereditary}" using T0_here IsHer_def by auto subsection‹Spectrum and anti-properties› text‹The spectrum of a topological property is a class of sets such that all topologies defined over that set have that property.› text‹The spectrum of a property gives us the list of sets for which the property doesn't give any topological information. Being in the spectrum of a topological property is an invariant in the category of sets and function; mening that equipollent sets are in the same spectra.› definition Spec ("_ {is in the spectrum of} _" 99) where "Spec(K,P) ≡ ∀T. ((T{is a topology} ∧ ⋃T≈K) ⟶ P(T))" lemma equipollent_spect: assumes "A≈B" "B {is in the spectrum of} P" shows "A {is in the spectrum of} P" proof- from assms(2) have "∀T. ((T{is a topology} ∧ ⋃T≈B) ⟶ P(T))" using Spec_def by auto then have "∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ P(T))" using eqpoll_trans[OF _ assms(1)] by auto then show ?thesis using Spec_def by auto qed theorem eqpoll_iff_spec: assumes "A≈B" shows "(B {is in the spectrum of} P) ⟷ (A {is in the spectrum of} P)" proof assume "B {is in the spectrum of} P" with assms equipollent_spect show "A {is in the spectrum of} P" by auto next assume "A {is in the spectrum of} P" moreover from assms have "B≈A" using eqpoll_sym by auto ultimately show "B {is in the spectrum of} P" using equipollent_spect by auto qed text‹From the previous statement, we see that the spectrum could be formed only by representative of clases of sets. If \emph{AC} holds, this means that the spectrum can be taken as a set or class of cardinal numbers.› text‹Here is an example of the spectrum. The proof lies in the indiscrite filter ‹{A}› that can be build for any set. In this proof, we see that without choice, there is no way to define the sepctrum of a property with cardinals because if a set is not comparable with any ordinal, its cardinal is defined as ‹0› without the set being empty.› theorem T4_spectrum: shows "(A {is in the spectrum of} isT4) ⟷ A ≲ 1" proof assume "A {is in the spectrum of} isT4" then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩_{4}}))" using Spec_def by auto { assume "A≠0" then obtain x where "x∈A" by auto then have "x∈⋃{A}" by auto moreover then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto moreover then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto then have top:"({A}∪{0}) {is a topology}" "⋃({A}∪{0})≈A" using eqpoll_refl by auto then have "({A}∪{0}) {is T⇩_{4}}" using reg by auto then have "({A}∪{0}) {is T⇩_{2}}" using topology0.T3_is_T2 topology0.T4_is_T3 topology0_def top by auto ultimately have "⋃{A}={x}" using filter_T2_imp_card1[of "{A}""x"] by auto then have "A={x}" by auto then have "A≈1" using singleton_eqpoll_1 by auto } moreover have "A=0 ⟶ A≈0" by auto ultimately have "A≈1∨A≈0" by blast then show "A≲1" using empty_lepollI eqpoll_imp_lepoll eq_lepoll_trans by auto next assume "A≲1" have "A=0∨A≠0" by auto then obtain E where "A=0∨E∈A" by auto then have "A≈0∨E∈A" by auto with ‹A≲1› have "A≈0∨A={E}" using lepoll_1_is_sing by auto then have "A≈0∨A≈1" using singleton_eqpoll_1 by auto { fix T assume AS:"T{is a topology}""⋃T≈A" { assume "A≈0" with AS have "T{is a topology}" and empty:"⋃T=0" using eqpoll_trans eqpoll_0_is_0 by auto then have "T{is T⇩_{2}}" using isT2_def by auto then have "T{is T⇩_{1}}" using T2_is_T1 by auto moreover from empty have "T⊆{0}" by auto with AS(1) have "T={0}" using empty_open by auto from empty have rr:"∀A. A{is closed in}T ⟶ A=0" using IsClosed_def by auto have "∃U∈T. ∃V∈T. 0⊆U∧0⊆V∧U∩V=0" using empty_open AS(1) by auto with rr have "∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶ (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))" by blast then have "T{is normal}" using IsNormal_def by auto with ‹T{is T⇩_{1}}› have "T{is T⇩_{4}}" using isT4_def by auto } moreover { assume "A≈1" with AS have "T{is a topology}" and NONempty:"⋃T≈1" using eqpoll_trans[of "⋃T""A""1"] by auto then have "⋃T≲1" using eqpoll_imp_lepoll by auto moreover { assume "⋃T=0" then have "0≈⋃T" by auto with NONempty have "0≈1" using eqpoll_trans by blast then have "0=1" using eqpoll_0_is_0 eqpoll_sym by auto then have "False" by auto } then have "⋃T≠0" by auto then obtain R where "R∈⋃T" by blast ultimately have "⋃T={R}" using lepoll_1_is_sing by auto { fix x y assume "x{is closed in}T""y{is closed in}T" "x∩y=0" then have "x⊆⋃T""y⊆⋃T" using IsClosed_def by auto then have "x=0∨y=0" using ‹x∩y=0› ‹⋃T={R}› by force { assume "x=0" then have "x⊆0""y⊆⋃T" using ‹y⊆⋃T› by auto moreover have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto } moreover { assume "x≠0" with ‹x=0∨y=0› have "y=0" by auto then have "x⊆⋃T""y⊆0" using ‹x⊆⋃T› by auto moreover have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto } ultimately have "(∃U∈T. ∃V∈T. x ⊆ U ∧ y ⊆ V ∧ U ∩ V = 0)" by blast } then have "T{is normal}" using IsNormal_def by auto moreover { fix x y assume "x∈⋃T""y∈⋃T""x≠y" with ‹⋃T={R}› have "False" by auto then have "∃U∈T. x∈U∧y∉U" by auto } then have "T{is T⇩_{1}}" using isT1_def by auto ultimately have "T{is T⇩_{4}}" using isT4_def by auto } ultimately have "T{is T⇩_{4}}" using ‹A≈0∨A≈1› by auto } then have "∀T. (T{is a topology} ∧ ⋃T ≈ A) ⟶ (T{is T⇩_{4}})" by auto then show "A {is in the spectrum of} isT4" using Spec_def by auto qed text‹If the topological properties are related, then so are the spectra.› lemma P_imp_Q_spec_inv: assumes "∀T. T{is a topology} ⟶ (Q(T) ⟶ P(T))" "A {is in the spectrum of} Q" shows "A {is in the spectrum of} P" proof- from assms(2) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ Q(T)" using Spec_def by auto with assms(1) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ P(T)" by auto then show ?thesis using Spec_def by auto qed text‹Since we already now the spectrum of $T_4$; if we now the spectrum of $T_0$, it should be easier to compute the spectrum of $T_1$, $T_2$ and $T_3$.› theorem T0_spectrum: shows "(A {is in the spectrum of} isT0) ⟷ A ≲ 1" proof assume "A {is in the spectrum of} isT0" then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩_{0}}))" using Spec_def by auto { assume "A≠0" then obtain x where "x∈A" by auto then have "x∈⋃{A}" by auto moreover then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto moreover then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})≈A" using eqpoll_refl by auto then have "({A}∪{0}) {is T⇩_{0}}" using reg by auto { fix y assume "y∈A""x≠y" with ‹({A}∪{0}) {is T⇩_{0}}› obtain U where "U∈({A}∪{0})" and dis:"(x ∈ U ∧ y ∉ U) ∨ (y ∈ U ∧ x ∉ U)" using isT0_def by auto then have "U=A" by auto with dis ‹y∈A› ‹x∈⋃{A}› have "False" by auto } then have "∀y∈A. y=x" by auto with ‹x∈⋃{A}› have "A={