(* 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_examples Topology_ZF_properties func1 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 @{text "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 IsRegular ("_{is regular}" 90) where "T{is regular} ≡ ∀A. A{is closed in}T ⟶ (∀x∈⋃T-A. ∃U∈T. ∃V∈T. A⊆U∧x∈V∧U∩V=0)" 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, op`(?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, op`(?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 @{text "{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 @{text "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={x}" by blast 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" { fix T assume "T{is a topology}" then have "(T{is T⇩_{4}})⟶(T{is T⇩_{0}})" using topology0.T4_is_T3 topology0.T3_is_T2 T2_is_T1 T1_is_T0 topology0_def by auto } then have "∀T. T{is a topology} ⟶ ((T{is T⇩_{4}})⟶(T{is T⇩_{0}}))" by auto then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT0)" using P_imp_Q_spec_inv[of "λT. (T{is T⇩_{4}})""λT. T{is T⇩_{0}}"] by auto then show "(A {is in the spectrum of} isT0)" using T4_spectrum `A≲1` by auto qed theorem T1_spectrum: shows "(A {is in the spectrum of} isT1) ⟷ A ≲ 1" proof- note T2_is_T1 topology0.T3_is_T2 topology0.T4_is_T3 then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT1)" using P_imp_Q_spec_inv[of "isT4""isT1"] topology0_def by auto moreover note T1_is_T0 then have "(A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of}isT0)" using P_imp_Q_spec_inv[of "isT1""isT0"] by auto moreover note T0_spectrum T4_spectrum ultimately show ?thesis by blast qed theorem T2_spectrum: shows "(A {is in the spectrum of} isT2) ⟷ A ≲ 1" proof- note topology0.T3_is_T2 topology0.T4_is_T3 then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT2)" using P_imp_Q_spec_inv[of "isT4""isT2"] topology0_def by auto moreover note T2_is_T1 then have "(A {is in the spectrum of} isT2) ⟶ (A {is in the spectrum of}isT1)" using P_imp_Q_spec_inv[of "isT2""isT1"] by auto moreover note T1_spectrum T4_spectrum ultimately show ?thesis by blast qed theorem T3_spectrum: shows "(A {is in the spectrum of} isT3) ⟷ A ≲ 1" proof- note topology0.T4_is_T3 then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT3)" using P_imp_Q_spec_inv[of "isT4""isT3"] topology0_def by auto moreover note topology0.T3_is_T2 then have "(A {is in the spectrum of} isT3) ⟶ (A {is in the spectrum of}isT2)" using P_imp_Q_spec_inv[of "isT3""isT2"] topology0_def by auto moreover note T2_spectrum T4_spectrum ultimately show ?thesis by blast qed theorem compact_spectrum: shows "(A {is in the spectrum of} (λT. (⋃T) {is compact in}T)) ⟷ Finite(A)" proof assume "A {is in the spectrum of} (λT. (⋃T) {is compact in}T)" then have reg:"∀T. T{is a topology} ∧ ⋃T≈A ⟶ ((⋃T) {is compact in}T)" using Spec_def by auto have "Pow(A){is a topology} ∧ ⋃Pow(A)=A" using Pow_is_top by auto then have "Pow(A){is a topology} ∧ ⋃Pow(A)≈A" using eqpoll_refl by auto with reg have "A{is compact in}Pow(A)" by auto moreover have "{{x}. x∈A}∈Pow(Pow(A))" by auto moreover have "⋃{{x}. x∈A}=A" by auto ultimately have "∃N∈FinPow({{x}. x∈A}). A⊆⋃N" using IsCompact_def by auto then obtain N where "N∈FinPow({{x}. x∈A})" "A⊆⋃N" by auto then have "N⊆{{x}. x∈A}" "Finite(N)" "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 with `Finite(N)` have "Finite({{x}. x∈A})" by auto let ?B="{⟨x,{x}⟩. x∈A}" have "?B:A→{{x}. x∈A}" unfolding Pi_def function_def by auto then have "?B:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality by auto then have "A≈{{x}. x∈A}" using eqpoll_def by auto with `Finite({{x}. x∈A})` show "Finite(A)" using eqpoll_imp_Finite_iff by auto next assume "Finite(A)" { fix T assume "T{is a topology}" "⋃T≈A" with `Finite(A)` have "Finite(⋃T)" using eqpoll_imp_Finite_iff by auto then have "Finite(Pow(⋃T))" using Finite_Pow by auto moreover have "T⊆Pow(⋃T)" by auto ultimately have "Finite(T)" using subset_Finite by auto { fix M assume "M∈Pow(T)""⋃T⊆⋃M" with `Finite(T)` have "Finite(M)" using subset_Finite by auto with `⋃T⊆⋃M` have "∃N∈FinPow(M). ⋃T⊆⋃N" using FinPow_def by auto } then have "(⋃T){is compact in}T" unfolding IsCompact_def by auto } then show "A {is in the spectrum of} (λT. (⋃T) {is compact in}T)" using Spec_def by auto qed text{*It is, at least for some people, surprising that the spectrum of some properties cannot be completely determined in \emph{ZF}.*} theorem compactK_spectrum: assumes "{the axiom of}K{choice holds for subsets}(Pow(K))" "Card(K)" shows "(A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))) ⟷ (A≲K)" proof assume "A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))" then have reg:"∀T. T{is a topology}∧⋃T≈A ⟶ ((⋃T){is compact of cardinal} csucc(K){in}T)" using Spec_def by auto then have "A{is compact of cardinal} csucc(K) {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(K))" 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(K)" by auto then obtain N where "N∈Pow({{x}. x∈A})" "A⊆⋃N" "N≺csucc(K)" by auto then have "N⊆{{x}. x∈A}" "N≺csucc(K)" "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(K)` have "A≺csucc(K)" using lesspoll_trans1 by auto then show "A≲K" using Card_less_csucc_eq_le assms(2) by auto next assume "A≲K" { fix T assume "T{is a topology}""⋃T≈A" have "Pow(⋃T){is a topology}" using Pow_is_top by auto { fix B assume AS:"B∈Pow(⋃T)" then have "{{i}. i∈B}⊆{{i} .i∈⋃T}" by auto moreover have "B=⋃{{i}. i∈B}" by auto ultimately have "∃S∈Pow({{i}. i∈⋃T}). B=⋃S" by auto then have "B∈{⋃U. U∈Pow({{i}. i∈⋃T})}" by auto } moreover { fix B assume AS:"B∈{⋃U. U∈Pow({{i}. i∈⋃T})}" then have "B∈Pow(⋃T)" by auto } ultimately have base:"{{x}. x∈⋃T} {is a base for}Pow(⋃T)" unfolding IsAbaseFor_def by auto let ?f="{⟨i,{i}⟩. i∈⋃T}" have f:"?f:⋃T→ {{x}. x∈⋃T}" using Pi_def function_def by auto moreover { fix w x assume as:"w∈⋃T""x∈⋃T""?f`w=?f`x" with f have "?f`w={w}" "?f`x={x}" using apply_equality by auto with as(3) have "w=x" by auto } with f have "?f:inj(⋃T,{{x}. x∈⋃T})" unfolding inj_def by auto moreover { fix xa assume "xa∈{{x}. x∈⋃T}" then obtain x where "x∈⋃T""xa={x}" by auto with f have "?f`x=xa" using apply_equality by auto with `x∈⋃T` have "∃x∈⋃T. ?f`x=xa" by auto } then have "∀xa∈{{x}. x∈⋃T}. ∃x∈⋃T. ?f`x=xa" by blast ultimately have "?f:bij(⋃T,{{x}. x∈⋃T})" unfolding bij_def surj_def by auto then have "⋃T≈{{x}. x∈⋃T}" using eqpoll_def by auto then have "{{x}. x∈⋃T}≈⋃T" using eqpoll_sym by auto with `⋃T≈A` have "{{x}. x∈⋃T}≈A" using eqpoll_trans by blast then have "{{x}. x∈⋃T}≲A" using eqpoll_imp_lepoll by auto with `A≲K` have "{{x}. x∈⋃T}≲K" using lepoll_trans by blast then have "{{x}. x∈⋃T}≺csucc(K)" using assms(2) Card_less_csucc_eq_le by auto with base have "Pow(⋃T) {is of second type of cardinal}csucc(K)" unfolding IsSecondOfCard_def by auto moreover have "⋃Pow(⋃T)=⋃T" by auto with calculation assms(1) `Pow(⋃T){is a topology}` have "(⋃T) {is compact of cardinal}csucc(K){in}Pow(⋃T)" using compact_of_cardinal_Q[of "K""Pow(⋃T)"] by auto moreover have "T⊆Pow(⋃T)" by auto ultimately have "(⋃T) {is compact of cardinal}csucc(K){in}T" using compact_coarser by auto } then show "A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal}csucc(K) {in}T))" using Spec_def by auto qed theorem compactK_spectrum_reverse: assumes "∀A. (A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))) ⟷ (A≲K)" "InfCard(K)" shows "{the axiom of}K{choice holds for subsets}(Pow(K))" proof- have "K≲K" using lepoll_refl by auto then have "K {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))" using assms(1) by auto moreover have "Pow(K){is a topology}" using Pow_is_top by auto moreover have "⋃Pow(K)=K" by auto then have "⋃Pow(K)≈K" using eqpoll_refl by auto ultimately have "K {is compact of cardinal} csucc(K){in}Pow(K)" using Spec_def by auto then show ?thesis using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ assms(2) by auto qed text{*This last theorem states that if one of the forms of the axiom of choice related to this compactness property fails, then the spectrum will be different. Notice that even for LindelÃ¶f spaces that will happend.*} text{*The spectrum gives us the posibility to define what an anti-property means. A space is anti-@{text "P"} if the only subspaces which have the property are the ones in the spectrum of @{text "P"}. This concept tries to put together spaces that are completely opposite to spaces where @{text "P(T)"}.*} definition antiProperty ("_{is anti-}_" 50) where "T{is anti-}P ≡ ∀A∈Pow(⋃T). P(T{restricted to}A) ⟶ (A {is in the spectrum of} P)" abbreviation "ANTI(P) ≡ λT. (T{is anti-}P)" text{*A first, very simple, but very useful result is the following: when the properties are related and the spectra are equal, then the anti-properties are related in the oposite direction.*} theorem (in topology0) eq_spect_rev_imp_anti: assumes "∀T. T{is a topology} ⟶ P(T) ⟶ Q(T)" "∀A. (A{is in the spectrum of}Q) ⟶ (A{is in the spectrum of}P)" and "T{is anti-}Q" shows "T{is anti-}P" proof- { fix A assume "A∈Pow(⋃T)""P(T{restricted to}A)" with assms(1) have "Q(T{restricted to}A)" using Top_1_L4 by auto with assms(3) `A∈Pow(⋃T)` have "A{is in the spectrum of}Q" using antiProperty_def by auto with assms(2) have "A{is in the spectrum of}P" by auto } then show ?thesis using antiProperty_def by auto qed text{*If a space can be @{text "P(T)∧Q(T)"} only in case the underlying set is in the spectrum of @{text "P"}; then @{text "Q(T)⟶ANTI(P,T)"} when @{text "Q"} is hereditary.*} theorem Q_P_imp_Spec: assumes "∀T. ((T{is a topology}∧P(T)∧Q(T))⟶ ((⋃T){is in the spectrum of}P))" and "Q{is hereditary}" shows "∀T. T{is a topology} ⟶ (Q(T)⟶(T{is anti-}P))" proof fix T { assume "T{is a topology}" { assume "Q(T)" { assume "¬(T{is anti-}P)" then obtain A where "A∈Pow(⋃T)" "P(T{restricted to}A)""¬(A{is in the spectrum of}P)" unfolding antiProperty_def by auto from `Q(T)``T{is a topology}``A∈Pow(⋃T)` assms(2) have "Q(T{restricted to}A)" unfolding IsHer_def by auto moreover note `P(T{restricted to}A)` assms(1) moreover from `T{is a topology}` have "(T{restricted to}A){is a topology}" using topology0.Top_1_L4 topology0_def by auto moreover from `A∈Pow(⋃T)` have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto ultimately have "A{is in the spectrum of}P" by auto with `¬(A{is in the spectrum of}P)` have "False" by auto } then have "T{is anti-}P" by auto } then have "Q(T)⟶(T{is anti-}P)" by auto } then show "(T {is a topology}) ⟶ (Q(T) ⟶ (T{is anti-}P))" by auto qed text{*If a topologycal space has an hereditary property, then it has its double-anti property.*} theorem (in topology0)her_P_imp_anti2P: assumes "P{is hereditary}" "P(T)" shows "T{is anti-}ANTI(P)" proof- { assume "¬(T{is anti-}ANTI(P))" then have "∃A∈Pow(⋃T). ((T{restricted to}A){is anti-}P)∧¬(A{is in the spectrum of}ANTI(P))" unfolding antiProperty_def[of _ "ANTI(P)"] by auto then obtain A where A_def:"A∈Pow(⋃T)""¬(A{is in the spectrum of}ANTI(P))""(T{restricted to}A){is anti-}P" by auto from `A∈Pow(⋃T)` have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto from A_def have reg:"∀B∈Pow(⋃(T{restricted to}A)). P((T{restricted to}A){restricted to}B) ⟶ (B{is in the spectrum of}P)" unfolding antiProperty_def by auto have "∀B∈Pow(A). (T{restricted to}A){restricted to}B=T{restricted to}B" using subspace_of_subspace `A∈Pow(⋃T)` by auto then have "∀B∈Pow(A). P(T{restricted to}B) ⟶ (B{is in the spectrum of}P)" using reg tot by force moreover have "∀B∈Pow(A). P(T{restricted to}B)" using assms `A∈Pow(⋃T)` unfolding IsHer_def using topSpaceAssum by blast ultimately have reg2:"∀B∈Pow(A). (B{is in the spectrum of}P)" by auto from `¬(A{is in the spectrum of}ANTI(P))` have "∃T. T{is a topology} ∧ ⋃T≈A ∧ ¬(T{is anti-}P)" unfolding Spec_def by auto then obtain S where "S{is a topology}" "⋃S≈A" "¬(S{is anti-}P)" by auto from `¬(S{is anti-}P)` have "∃B∈Pow(⋃S). P(S{restricted to}B) ∧ ¬(B{is in the spectrum of}P)" unfolding antiProperty_def by auto then obtain B where B_def:"¬(B{is in the spectrum of}P)" "B∈Pow(⋃S)" by auto then have "B≲⋃S" using subset_imp_lepoll by auto with `⋃S≈A` have "B≲A" using lepoll_eq_trans by auto then obtain f where "f∈inj(B,A)" unfolding lepoll_def by auto then have "f∈bij(B,range(f))" using inj_bij_range by auto then have "B≈range(f)" unfolding eqpoll_def by auto with B_def(1) have "¬(range(f){is in the spectrum of}P)" using eqpoll_iff_spec by auto moreover with `f∈inj(B,A)` have "range(f)⊆A" unfolding inj_def Pi_def by auto with reg2 have "range(f){is in the spectrum of}P" by auto ultimately have "False" by auto } then show ?thesis by auto qed text{*The anti-properties are always hereditary*} theorem anti_here: shows "ANTI(P){is hereditary}" proof- { fix T assume "T {is a topology}""ANTI(P,T)" { fix A assume "A∈Pow(⋃T)" then have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto moreover { fix B assume "B∈Pow(A)""P((T{restricted to}A){restricted to}B)" with `A∈Pow(⋃T)` have "B∈Pow(⋃T)""P(T{restricted to}B)" using subspace_of_subspace by auto with `ANTI(P,T)` have "B{is in the spectrum of}P" unfolding antiProperty_def by auto } ultimately have "∀B∈Pow(⋃(T{restricted to}A)). (P((T{restricted to}A){restricted to}B)) ⟶ (B{is in the spectrum of}P)" by auto then have "ANTI(P,(T{restricted to}A))" unfolding antiProperty_def by auto } then have "∀A∈Pow(⋃T). ANTI(P,(T{restricted to}A))" by auto } then show ?thesis using IsHer_def by auto qed corollary (in topology0) anti_imp_anti3: assumes "T{is anti-}P" shows "T{is anti-}ANTI(ANTI(P))" using anti_here her_P_imp_anti2P assms by auto text{*In the article \cite{ReVa80}, we can find some results on anti-properties.*} theorem (in topology0) anti_T0: shows "(T{is anti-}isT0) ⟷ T={0,⋃T}" proof assume "T={0,⋃T}" { fix A assume "A∈Pow(⋃T)""(T{restricted to}A) {is T⇩_{0}}" { fix B assume "B∈T{restricted to}A" then obtain S where "S∈T" and "B=A∩S" unfolding RestrictedTo_def by auto with `T={0,⋃T}` have "S∈{0,⋃T}" by auto then have "S=0∨S=⋃T" by auto with `B=A∩S``A∈Pow(⋃T)` have "B=0∨B=A" by auto } moreover { have "0∈{0,⋃T}" "⋃T∈{0,⋃T}" by auto with `T={0,⋃T}` have "0∈T""(⋃T)∈T" by auto then have "A∩0∈(T{restricted to}A)" "A∩(⋃T)∈(T{restricted to}A)" using RestrictedTo_def by auto moreover from `A∈Pow(⋃T)` have "A∩(⋃T)=A" by auto ultimately have "0∈(T{restricted to}A)" "A∈(T{restricted to}A)" by auto } ultimately have "(T{restricted to}A)={0,A}" by auto with `(T{restricted to}A) {is T⇩_{0}}` have "{0,A} {is T⇩_{0}}" by auto { assume "A≠0" then obtain x where "x∈A" by blast { fix y assume "y∈A""x≠y" with `{0,A} {is T⇩_{0}}` obtain U where "U∈{0,A}" 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={x}" by blast then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto then have "A{is in the spectrum of}isT0" using T0_spectrum by auto } moreover { assume "A=0" then have "A≈0" by auto then have "A≲1" using empty_lepollI eq_lepoll_trans by auto then have "A{is in the spectrum of}isT0" using T0_spectrum by auto } ultimately have "A{is in the spectrum of}isT0" by auto } then show "T{is anti-}isT0" using antiProperty_def by auto next assume "T{is anti-}isT0" then have "∀A∈Pow(⋃T). (T{restricted to}A){is T⇩_{0}} ⟶ (A{is in the spectrum of}isT0)" using antiProperty_def by auto then have reg:"∀A∈Pow(⋃T). (T{restricted to}A){is T⇩_{0}} ⟶ (A≲1)" using T0_spectrum by auto { assume "∃A∈T. A≠0∧ A≠⋃T" then obtain A where "A∈T""A≠0""A≠⋃T" by auto then obtain x y where "x∈A" "y∈⋃T-A" by blast with `A∈T` have s:"{x,y}∈Pow(⋃T)" "x≠y" by auto note s moreover { fix b1 b2 assume "b1∈⋃(T{restricted to}{x,y})""b2∈⋃(T{restricted to}{x,y})""b1≠b2" moreover from s have "⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto ultimately have "(b1=x∧b2=y)∨(b1=y∧b2=x)" by auto with `x≠y` have "(b1∈{x}∧b2∉{x}) ∨ (b2∈{x}∧b1∉{x})" by auto moreover from `y∈⋃T-A``x∈A` have "{x}={x,y}∩A" by auto with `A∈T` have "{x}∈(T{restricted to}{x,y})" unfolding RestrictedTo_def by auto ultimately have "∃U∈(T{restricted to}{x,y}). (b1∈U∧b2∉U) ∨ (b2∈U∧b1∉U)" by auto } then have "(T{restricted to}{x,y}){is T⇩_{0}}" using isT0_def by auto ultimately have "{x,y}≲1" using reg by auto moreover have "x∈{x,y}" by auto ultimately have "{x,y}={x}" using lepoll_1_is_sing[of "{x,y}""x"] by auto moreover have "y∈{x,y}" by auto ultimately have "y∈{x}" by auto then have "y=x" by auto with `x≠y` have "False" by auto } then have "T⊆{0,⋃T}" by auto moreover from topSpaceAssum have "0∈T""⋃T∈T" using IsATopology_def empty_open by auto ultimately show "T={0,⋃T}" by auto qed lemma indiscrete_spectrum: shows "(A {is in the spectrum of}(λT. T={0,⋃T})) ⟷ A≲1" proof assume "(A {is in the spectrum of}(λT. T={0,⋃T}))" then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ T ={0,⋃T})" using Spec_def by auto moreover have "⋃Pow(A)=A" by auto then have "⋃Pow(A)≈A" by auto moreover have "Pow(A) {is a topology}" using Pow_is_top by auto ultimately have P:"Pow(A)={0,A}" by auto { assume "A≠0" then obtain x where "x∈A" by blast then have "{x}∈Pow(A)" by auto with P have "{x}=A" by auto then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto } moreover { assume "A=0" then have "A≈0" by auto then have "A≲1" using empty_lepollI eq_lepoll_trans by auto } ultimately show "A≲1" by auto next assume "A≲1" { fix T assume "T{is a topology}""⋃T≈A" { assume "A=0" with `⋃T≈A` have "⋃T≈0" by auto then have "⋃T=0" using eqpoll_0_is_0 by auto then have "T⊆{0}" by auto with `T{is a topology}` have "T={0}" using empty_open by auto then have "T={0,⋃T}" by auto } moreover { assume "A≠0" then obtain E where "E∈A" by blast with `A≲1` have "A={E}" using lepoll_1_is_sing by auto then have "A≈1" using singleton_eqpoll_1 by auto with `⋃T≈A` have NONempty:"⋃T≈1" using eqpoll_trans by blast 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 moreover have "T⊆Pow(⋃T)" by auto ultimately have "T⊆Pow({R})" by auto then have "T⊆{0,{R}}" by blast moreover with `T{is a topology}` have "0∈T""⋃T∈T" using IsATopology_def by auto moreover note `⋃T={R}` ultimately have "T={0,⋃T}" by auto } ultimately have "T={0,⋃T}" by auto } then show "A {is in the spectrum of}(λT. T={0,⋃T})" using Spec_def by auto qed theorem (in topology0) anti_indiscrete: shows "(T{is anti-}(λT. T={0,⋃T})) ⟷ T{is T⇩_{0}}" proof assume "T{is T⇩_{0}}" { fix A assume "A∈Pow(⋃T)""T{restricted to}A={0,⋃(T{restricted to}A)}" then have un:"⋃(T{restricted to}A)=A" "T{restricted to}A={0,A}" using RestrictedTo_def by auto from `T{is T⇩_{0}}``A∈Pow(⋃T)` have "(T{restricted to}A){is T⇩_{0}}" using T0_here by auto { assume "A=0" then have "A≈0" by auto then have "A≲1" using empty_lepollI eq_lepoll_trans by auto } moreover { assume "A≠0" then obtain E where "E∈A" by blast { fix y assume "y∈A""y≠E" with `E∈A` un have "y∈⋃(T{restricted to}A)""E∈⋃(T{restricted to}A)" by auto with `(T{restricted to}A){is T⇩_{0}}``y≠E` have "∃U∈(T{restricted to}A). (E∈U∧y∉U)∨(E∉U∧y∈U)" unfolding isT0_def by blast then obtain U where "U∈(T{restricted to}A)" "(E∈U∧y∉U)∨(E∉U∧y∈U)" by auto with `T{restricted to}A={0,A}` have "U=0∨U=A" by auto with `(E∈U∧y∉U)∨(E∉U∧y∈U)``y∈A``E∈A` have "False" by auto } then have "∀y∈A. y=E" by auto with `E∈A` have "A={E}" by blast then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto } ultimately have "A≲1" by auto then have "A{is in the spectrum of}(λT. T={0,⋃T})" using indiscrete_spectrum by auto } then show "T{is anti-}(λT. T={0,⋃T})" unfolding antiProperty_def by auto next assume "T{is anti-}(λT. T={0,⋃T})" then have "∀A∈Pow(⋃T). (T{restricted to}A)={0,⋃(T{restricted to}A)} ⟶ (A {is in the spectrum of} (λT. T={0,⋃T}))" using antiProperty_def by auto then have "∀A∈Pow(⋃T). (T{restricted to}A)={0,⋃(T{restricted to}A)} ⟶ A≲1" using indiscrete_spectrum by auto moreover have "∀A∈Pow(⋃T). ⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto ultimately have reg:"∀A∈Pow(⋃T). (T{restricted to}A)={0,A} ⟶ A≲1" by auto { fix x y assume "x∈⋃T""y∈⋃T""x≠y" { assume "∀U∈T. (x∈U∧y∈U)∨(x∉U∧y∉U)" then have "T{restricted to}{x,y}⊆{0,{x,y}}" unfolding RestrictedTo_def by auto moreover from `x∈⋃T``y∈⋃T` have emp:"0∈T""{x,y}∩0=0" and tot: "{x,y}={x,y}∩⋃T" "⋃T∈T" using topSpaceAssum empty_open IsATopology_def by auto from emp have "0∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto moreover from tot have "{x,y}∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto ultimately have "T{restricted to}{x,y}={0,{x,y}}" by auto with reg `x∈⋃T``y∈⋃T` have "{x,y}≲1" by auto moreover have "x∈{x,y}" by auto ultimately have "{x,y}={x}" using lepoll_1_is_sing[of "{x,y}""x"] by auto moreover have "y∈{x,y}" by auto ultimately have "y∈{x}" by auto then have "y=x" by auto then have "False" using `x≠y` by auto } then have "∃U∈T. (x∉U∨y∉U)∧(x∈U∨y∈U)" by auto then have "∃U∈T. (x∈U∧y∉U)∨(x∉U∧y∈U)" by auto } then have "∀x y. x∈⋃T∧y∈⋃T∧ x≠y ⟶ (∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U))" by auto then show "T {is T⇩_{0}}" using isT0_def by auto qed text{*The conclusion is that being $T_0$ is just the opposite to being indiscrete.*} text{*Next, let's compute the anti-$T_i$ for $i=1,\ 2,\ 3$ or $4$. Surprisingly, they are all the same. Meaning, that the total negation of $T_1$ is enough to negate all of these axioms.*} theorem anti_T1: shows "(T{is anti-}isT1) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" proof assume "T{is anti-}isT1" let ?r="{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}" have "antisym(?r)" unfolding antisym_def by auto moreover have "trans(?r)" unfolding trans_def by auto moreover { fix A B assume "A∈T""B∈T" { assume "¬(A⊆B∨B⊆A)" then have "A-B≠0""B-A≠0" by auto then obtain x y where "x∈A""x∉B""y∈B""y∉A" "x≠y" by blast then have "{x,y}∩A={x}""{x,y}∩B={y}" by auto moreover from `A∈T``B∈T` have "{x,y}∩A∈T{restricted to}{x,y}""{x,y}∩B∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto ultimately have open_set:"{x}∈T{restricted to}{x,y}""{y}∈T{restricted to}{x,y}" by auto have "x∈⋃T""y∈⋃T" using `A∈T``B∈T``x∈A``y∈B` by auto then have sub:"{x,y}∈Pow(⋃T)" by auto then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto { fix s t assume "s∈⋃(T{restricted to}{x,y})""t∈⋃(T{restricted to}{x,y})""s≠t" with tot have "s∈{x,y}""t∈{x,y}""s≠t" by auto then have "(s=x∧t=y)∨(s=y∧t=x)" by auto with open_set have "∃U∈(T{restricted to}{x,y}). s∈U∧t∉U" using `x≠y` by auto } then have "(T{restricted to}{x,y}){is T⇩_{1}}" unfolding isT1_def by auto with sub `T{is anti-}isT1` tot have "{x,y} {is in the spectrum of}isT1" using antiProperty_def by auto then have "{x,y}≲1" using T1_spectrum by auto moreover have "x∈{x,y}" by auto ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto moreover have "y∈{x,y}" by auto ultimately have "y∈{x}" by auto then have "x=y" by auto then have "False" using `x∈A``y∉A` by auto } then have "A⊆B∨B⊆A" by auto } then have "?r {is total on}T" using IsTotal_def by auto ultimately show "IsLinOrder(T,?r)" using IsLinOrder_def by auto next assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" then have ordTot:"∀S∈T. ∀B∈T. S⊆B∨B⊆S" unfolding IsLinOrder_def IsTotal_def by auto { fix A assume "A∈Pow(⋃T)" and T1:"(T{restricted to}A) {is T⇩_{1}}" then have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto { fix U V assume "U∈T{restricted to}A""V∈T{restricted to}A" then obtain AU AV where "AU∈T""AV∈T""U=A∩AU""V=A∩AV" unfolding RestrictedTo_def by auto with ordTot have "U⊆V∨V⊆U" by auto } then have ordTotSub:"∀S∈T{restricted to}A. ∀B∈T{restricted to}A. S⊆B∨B⊆S" by auto { assume "A=0" then have "A≈0" by auto moreover have "0≲1" using empty_lepollI by auto ultimately have "A≲1" using eq_lepoll_trans by auto then have "A{is in the spectrum of}isT1" using T1_spectrum by auto } moreover { assume "A≠0" then obtain t where "t∈A" by blast { fix y assume "y∈A""y≠t" with `t∈A` tot T1 obtain U where "U∈(T{restricted to}A)""y∈U""t∉U" unfolding isT1_def by auto from `y≠t` have "t≠y" by auto with `y∈A``t∈A` tot T1 obtain V where "V∈(T{restricted to}A)""t∈V""y∉V" unfolding isT1_def by auto with `y∈U``t∉U` have "¬(U⊆V∨V⊆U)" by auto with ordTotSub `U∈(T{restricted to}A)``V∈(T{restricted to}A)` have "False" by auto } then have "∀y∈A. y=t" by auto with `t∈A` have "A={t}" by blast then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto then have "A{is in the spectrum of}isT1" using T1_spectrum by auto } ultimately have "A{is in the spectrum of}isT1" by auto } then show "T{is anti-}isT1" using antiProperty_def by auto qed corollary linordtop_here: shows "(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})){is hereditary}" using anti_T1 anti_here[of "isT1"] by auto theorem (in topology0) anti_T4: shows "(T{is anti-}isT4) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" proof assume "T{is anti-}isT4" let ?r="{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}" have "antisym(?r)" unfolding antisym_def by auto moreover have "trans(?r)" unfolding trans_def by auto moreover { fix A B assume "A∈T""B∈T" { assume "¬(A⊆B∨B⊆A)" then have "A-B≠0""B-A≠0" by auto then obtain x y where "x∈A""x∉B""y∈B""y∉A" "x≠y" by blast then have "{x,y}∩A={x}""{x,y}∩B={y}" by auto moreover from `A∈T``B∈T` have "{x,y}∩A∈T{restricted to}{x,y}""{x,y}∩B∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto ultimately have open_set:"{x}∈T{restricted to}{x,y}""{y}∈T{restricted to}{x,y}" by auto have "x∈⋃T""y∈⋃T" using `A∈T``B∈T``x∈A``y∈B` by auto then have sub:"{x,y}∈Pow(⋃T)" by auto then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto { fix s t assume "s∈⋃(T{restricted to}{x,y})""t∈⋃(T{restricted to}{x,y})""s≠t" with tot have "s∈{x,y}""t∈{x,y}""s≠t" by auto then have "(s=x∧t=y)∨(s=y∧t=x)" by auto with open_set have "∃U∈(T{restricted to}{x,y}). s∈U∧t∉U" using `x≠y` by auto } then have "(T{restricted to}{x,y}){is T⇩_{1}}" unfolding isT1_def by auto moreover { fix s assume AS:"s{is closed in}(T{restricted to}{x,y})" { fix t assume AS2:"t{is closed in}(T{restricted to}{x,y})""s∩t=0" have "(T{restricted to}{x,y}){is a topology}" using Top_1_L4 by auto with tot have "0∈(T{restricted to}{x,y})""{x,y}∈(T{restricted to}{x,y})" using empty_open union_open[where 𝒜="T{restricted to}{x,y}"] by auto moreover note open_set moreover have "T{restricted to}{x,y}⊆Pow(⋃(T{restricted to}{x,y}))" by blast with tot have "T{restricted to}{x,y}⊆Pow({x,y})" by auto ultimately have "T{restricted to}{x,y}={0,{x},{y},{x,y}}" by blast moreover have "{0,{x},{y},{x,y}}=Pow({x,y})" by blast ultimately have P:"T{restricted to}{x,y}=Pow({x,y})" by simp with tot have "{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}={A ∈ Pow({x, y}) . A ⊆ {x, y} ∧ {x, y} - A ∈ Pow({x, y})}" using IsClosed_def by simp with P have S:"{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}=T{restricted to}{x,y}" by auto from AS AS2(1) have "s∈Pow({x,y})" "t∈Pow({x,y})" using IsClosed_def tot by auto moreover note AS2(1) AS ultimately have "s∈{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}""t∈{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}" by auto with S AS2(2) have "s∈T{restricted to}{x,y}" "t∈T{restricted to}{x,y}""s∩t=0" by auto then have "∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0" by auto } then have "∀t. t{is closed in}(T{restricted to}{x,y})∧s∩t=0 ⟶ (∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0)" by auto } then have "∀s. s{is closed in}(T{restricted to}{x,y}) ⟶ (∀t. t{is closed in}(T{restricted to}{x,y})∧s∩t=0 ⟶ (∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0))" by auto then have "(T{restricted to}{x,y}){is normal}" using IsNormal_def by auto ultimately have "(T{restricted to}{x,y}){is T⇩_{4}}" using isT4_def by auto with sub `T{is anti-}isT4` tot have "{x,y} {is in the spectrum of}isT4" using antiProperty_def by auto then have "{x,y}≲1" using T4_spectrum by auto moreover have "x∈{x,y}" by auto ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto moreover have "y∈{x,y}" by auto ultimately have "y∈{x}" by auto then have "x=y" by auto then have "False" using `x∈A``y∉A` by auto } then have "A⊆B∨B⊆A" by auto } then have "?r {is total on}T" using IsTotal_def by auto ultimately show "IsLinOrder(T,?r)" using IsLinOrder_def by auto next assume "IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V})" then have "T{is anti-}isT1" using anti_T1 by auto moreover have "∀T. T{is a topology} ⟶ (T{is T⇩_{4}}) ⟶ (T{is T⇩_{1}})" using topology0.T4_is_T3 topology0.T3_is_T2 T2_is_T1 topology0_def by auto moreover have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT4)" using T1_spectrum T4_spectrum by auto ultimately show "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT1"] by auto qed theorem (in topology0) anti_T3: shows "(T{is anti-}isT3) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" proof assume "T{is anti-}isT3" moreover have "∀T. T{is a topology} ⟶ (T{is T⇩_{4}}) ⟶ (T{is T⇩_{3}})" using topology0.T4_is_T3 topology0_def by auto moreover have " ∀A. (A {is in the spectrum of} isT3) ⟶ (A {is in the spectrum of} isT4)" using T3_spectrum T4_spectrum by auto ultimately have "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT3"] by auto then show "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" using anti_T4 by auto next assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" then have "T{is anti-}isT1" using anti_T1 by auto moreover have "∀T. T{is a topology} ⟶ (T{is T⇩_{3}}) ⟶ (T{is T⇩_{1}})" using topology0.T3_is_T2 T2_is_T1 topology0_def by auto moreover have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT3)" using T1_spectrum T3_spectrum by auto ultimately show "T{is anti-}isT3" using eq_spect_rev_imp_anti[of "isT3""isT1"] by auto qed theorem (in topology0) anti_T2: shows "(T{is anti-}isT2) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" proof assume "T{is anti-}isT2" moreover have "∀T. T{is a topology} ⟶ (T{is T⇩_{4}}) ⟶ (T{is T⇩_{2}})" using topology0.T4_is_T3 topology0.T3_is_T2 topology0_def by auto moreover have " ∀A. (A {is in the spectrum of} isT2) ⟶ (A {is in the spectrum of} isT4)" using T2_spectrum T4_spectrum by auto ultimately have "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT2"] by auto then show "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" using anti_T4 by auto next assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" then have "T{is anti-}isT1" using anti_T1 by auto moreover have "∀T. T{is a topology} ⟶ (T{is T⇩_{2}}) ⟶ (T{is T⇩_{1}})" using T2_is_T1 by auto moreover have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT2)" using T1_spectrum T2_spectrum by auto ultimately show "T{is anti-}isT2" using eq_spect_rev_imp_anti[of "isT2""isT1"] by auto qed lemma linord_spectrum: shows "(A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))) ⟷ A≲1" proof assume "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" then have reg:"∀T. T{is a topology}∧ ⋃T≈A ⟶ IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" using Spec_def by auto { assume "A=0" moreover have "0≲1" using empty_lepollI by auto ultimately have "A≲1" using eq_lepoll_trans by auto } moreover { assume "A≠0" then obtain x where "x∈A" by blast moreover { fix y assume "y∈A" have "Pow(A) {is a topology}" using Pow_is_top by auto moreover have "⋃Pow(A)=A" by auto then have "⋃Pow(A)≈A" by auto note reg ultimately have "IsLinOrder(Pow(A),{⟨U,V⟩∈Pow(⋃Pow(A))×Pow(⋃Pow(A)). U⊆V})" by auto then have "IsLinOrder(Pow(A),{⟨U,V⟩∈Pow(A)×Pow(A). U⊆V})" by auto with `x∈A``y∈A` have "{x}⊆{y}∨{y}⊆{x}" unfolding IsLinOrder_def IsTotal_def by auto then have "x=y" by auto } ultimately have "A={x}" by blast then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto } ultimately show "A≲1" by auto next assume "A≲1" then have ind:"A{is in the spectrum of}(λT. T={0,⋃T})" using indiscrete_spectrum by auto { fix T assume AS:"T{is a topology}" "T={0,⋃T}" have "trans({⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding trans_def by auto moreover have "antisym({⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding antisym_def by auto moreover have "{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}{is total on}T" proof- { fix aa b assume "aa∈T""b∈T" with AS(2) have "aa∈{0,⋃T}""b∈{0,⋃T}" by auto then have "aa=0∨aa=⋃T""b=0∨b=⋃T" by auto then have "aa⊆b∨b⊆aa" by auto then have "⟨aa, b⟩ ∈ Collect(Pow(⋃T) × Pow(⋃T), split(op ⊆)) ∨ ⟨b, aa⟩ ∈ Collect(Pow(⋃T) × Pow(⋃T), split(op ⊆))" using `aa∈T``b∈T` by auto } then show ?thesis using IsTotal_def by auto qed ultimately have "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding IsLinOrder_def by auto } then have " ∀T. T {is a topology} ⟶ T = {0, ⋃T} ⟶ IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V})" by auto then show "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" using P_imp_Q_spec_inv[of "λT. T={0,⋃T}""λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"] ind by auto qed theorem (in topology0) anti_linord: shows "(T{is anti-}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))) ⟷ T{is T⇩_{1}}" proof assume AS:"T{is anti-}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" { assume "¬(T{is T⇩_{1}})" then obtain x y where "x∈⋃T""y∈⋃T""x≠y""∀U∈T. x∉U∨y∈U" unfolding isT1_def by auto { assume "{x}∈T{restricted to}{x,y}" then obtain U where "U∈T" "{x}={x,y}∩U" unfolding RestrictedTo_def by auto moreover have "x∈{x}" by auto ultimately have "U∈T""x∈U" by auto moreover { assume "y∈U" then have "y∈{x,y}∩U" by auto with `{x}={x,y}∩U` have "y∈{x}" by auto with `x≠y` have "False" by auto } then have "y∉U" by auto moreover note `∀U∈T. x∉U∨y∈U` ultimately have "False" by auto } then have "{x}∉T{restricted to}{x,y}" by auto moreover have tot:"⋃(T{restricted to}{x,y})={x,y}" using `x∈⋃T``y∈⋃T` unfolding RestrictedTo_def by auto moreover have "T{restricted to}{x,y}⊆Pow(⋃(T{restricted to}{x,y}))" by auto ultimately have "T{restricted to}{x,y}⊆Pow({x,y})-{{x}}" by auto moreover have "Pow({x,y})={0,{x,y},{x},{y}}" by blast ultimately have "T{restricted to}{x,y}⊆{0,{x,y},{y}}" by auto moreover have "IsLinOrder({0,{x,y},{y}},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" proof- have "antisym(Collect(Pow({x, y}) × Pow({x, y}), split(op ⊆)))" using antisym_def by auto moreover have "trans(Collect(Pow({x, y}) × Pow({x, y}), split(op ⊆)))" using trans_def by auto moreover have "Collect(Pow({x, y}) × Pow({x, y}), split(op ⊆)) {is total on} {0, {x, y}, {y}}" using IsTotal_def by auto ultimately show "IsLinOrder({0,{x,y},{y}},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" using IsLinOrder_def by auto qed ultimately have "IsLinOrder(T{restricted to}{x,y},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" using ord_linear_subset by auto with tot have "IsLinOrder(T{restricted to}{x,y},{⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V})" by auto then have "IsLinOrder(T{restricted to}{x,y},Collect(Pow(⋃(T {restricted to} {x,y})) × Pow(⋃(T {restricted to} {x,y})), split(op ⊆)))" by auto moreover from `x∈⋃T``y∈⋃T` have "{x,y}∈Pow(⋃T)" by auto moreover note AS ultimately have "{x,y}{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" unfolding antiProperty_def by simp then have "{x,y}≲1" using linord_spectrum by auto moreover have "x∈{x,y}" by auto ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto moreover have "y∈{x,y}" by auto ultimately have "y∈{x}" by auto then have "x=y" by auto then have "False" using `x≠y` by auto } then show "T {is T⇩_{1}}" by auto next assume T1:"T {is T⇩_{1}}" { fix A assume A_def:"A∈Pow(⋃T)""IsLinOrder((T{restricted to}A) ,{⟨U,V⟩∈Pow(⋃(T{restricted to}A))×Pow(⋃(T{restricted to}A)). U⊆V})" { fix x assume AS1:"x∈A" { fix y assume AS:"y∈A""x≠y" with AS1 have "{x,y}∈Pow(⋃T)" using `A∈Pow(⋃T)` by auto from `x∈A``y∈A` have "{x,y}∈Pow(A)" by auto from `{x,y}∈Pow(⋃T)` have T11:"(T{restricted to}{x,y}){is T⇩_{1}}" using T1_here T1 by auto moreover have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def using `{x,y}∈Pow(⋃T)` by auto moreover note AS(2) ultimately obtain U where "x∈U""y∉U""U∈(T{restricted to}{x,y})" unfolding isT1_def by auto moreover from AS(2) tot T11 obtain V where "y∈V""x∉V""V∈(T{restricted to}{x,y})" unfolding isT1_def by auto ultimately have "x∈U-V""y∈V-U""U∈(T{restricted to}{x,y})""V∈(T{restricted to}{x,y})" by auto then have "¬(U⊆V∨V⊆U)""U∈(T{restricted to}{x,y})""V∈(T{restricted to}{x,y})" by auto then have "¬({⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V} {is total on} (T{restricted to}{x,y}))" unfolding IsTotal_def by auto then have "¬(IsLinOrder((T{restricted to}{x,y}),{⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V}))" unfolding IsLinOrder_def by auto moreover { have "(T{restricted to}A) {is a topology}" using Top_1_L4 by auto moreover note A_def(2) linordtop_here ultimately have "∀B∈Pow(⋃(T{restricted to}A)). IsLinOrder((T{restricted to}A){restricted to}B ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})" unfolding IsHer_def by auto moreover have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def using `A∈Pow(⋃T)` by auto ultimately have "∀B∈Pow(A). IsLinOrder((T{restricted to}A){restricted to}B ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})" by auto moreover have "∀B∈Pow(A). (T{restricted to}A){restricted to}B=T{restricted to}B" using subspace_of_subspace `A∈Pow(⋃T)` by auto ultimately have "∀B∈Pow(A). IsLinOrder((T{restricted to}B) ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})" by auto moreover have "∀B∈Pow(A). ⋃((T{restricted to}A){restricted to}B)=B" using `A∈Pow(⋃T)` unfolding RestrictedTo_def by auto ultimately have "∀B∈Pow(A). IsLinOrder((T{restricted to}B) ,{⟨U,V⟩∈Pow(B)×Pow(B). U⊆V})" by auto with `{x,y}∈Pow(A)` have "IsLinOrder((T{restricted to}{x,y}) ,{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" by auto } ultimately have "False" using tot by auto } then have "A={x}" using AS1 by auto then have "A≈1" using singleton_eqpoll_1 by auto then have "A≲1" using eqpoll_imp_lepoll by auto then have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" using linord_spectrum by auto } moreover { assume "A=0" then have "A≈0" by auto moreover have "0≲1" using empty_lepollI by auto ultimately have "A≲1" using eq_lepoll_trans by auto then have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" using linord_spectrum by auto } ultimately have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" by blast } then show "T{is anti-}(λT. IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V}))" unfolding antiProperty_def by auto qed text{*In conclusion, $T_1$ is also an anti-property.*} text{*Let's define some anti-properties that we'll use in the future.*} definition IsAntiComp ("_{is anti-compact}") where "T{is anti-compact} ≡ T{is anti-}(λT. (⋃T){is compact in}T)" definition IsAntiLin ("_{is anti-lindeloef}") where "T{is anti-lindeloef} ≡ T{is anti-}(λT. ((⋃T){is lindeloef in}T))" text{*Anti-compact spaces are also called pseudo-finite spaces in literature before the concept of anti-property was defined.*} end