(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2012 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 7› theory Topology_ZF_7 imports Topology_ZF_5 begin subsection{*Connection Properties*} text{*Another type of topological properties are the connection properties. These properties establish if the space is formed of several pieces or just one.*} text{*A space is connected iff there is no clopen set other that the empty set and the total set.*} definition IsConnected ("_{is connected}" 70) where "T {is connected} ≡ ∀U. (U∈T ∧ (U {is closed in}T)) ⟶ U=0∨U=⋃T" lemma indiscrete_connected: shows "{0,X} {is connected}" unfolding IsConnected_def IsClosed_def by auto text{*The anti-property of connectedness is called total-diconnectedness.*} definition IsTotDis ("_ {is totally-disconnected}" 70) where "IsTotDis ≡ ANTI(IsConnected)" lemma conn_spectrum: shows "(A{is in the spectrum of}IsConnected) ⟷ A≲1" proof assume "A{is in the spectrum of}IsConnected" then have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is connected})" using Spec_def by auto moreover 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 ultimately have "Pow(A) {is connected}" by auto { assume "A≠0" then obtain E where "E∈A" by blast then have "{E}∈Pow(A)" by auto moreover have "A-{E}∈Pow(A)" by auto ultimately have "{E}∈Pow(A)∧{E}{is closed in}Pow(A)" unfolding IsClosed_def by auto with `Pow(A) {is connected}` have "{E}=A" unfolding IsConnected_def 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≲1" using empty_lepollI[of "1"] by auto } ultimately show "A≲1" by auto next assume "A≲1" { fix T assume "T{is a topology}""⋃T≈A" { assume "⋃T=0" with `T{is a topology}` have "T={0}" using empty_open by auto then have "T{is connected}" unfolding IsConnected_def by auto } moreover { assume "⋃T≠0" moreover from `A≲1``⋃T≈A` have "⋃T≲1" using eq_lepoll_trans by auto ultimately obtain E where "⋃T={E}" using lepoll_1_is_sing by blast moreover have "T⊆Pow(⋃T)" by auto ultimately have "T⊆Pow({E})" by auto then have "T⊆{0,{E}}" by blast with `T{is a topology}` have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto then have "T{is connected}" unfolding IsConnected_def by auto } ultimately have "T{is connected}" by auto } then show "A{is in the spectrum of}IsConnected" unfolding Spec_def by auto qed text{*The discrete space is a first example of totally-disconnected space.*} lemma discrete_tot_dis: shows "Pow(X) {is totally-disconnected}" proof- { fix A assume "A∈Pow(X)" and con:"(Pow(X){restricted to}A){is connected}" have res:"(Pow(X){restricted to}A)=Pow(A)" unfolding RestrictedTo_def using `A∈Pow(X)` by blast { assume "A=0" then have "A≲1" using empty_lepollI[of "1"] by auto then have "A{is in the spectrum of}IsConnected" using conn_spectrum by auto } moreover { assume "A≠0" then obtain E where "E∈A" by blast then have "{E}∈Pow(A)" by auto moreover have "A-{E}∈Pow(A)" by auto ultimately have "{E}∈Pow(A)∧{E}{is closed in}Pow(A)" unfolding IsClosed_def by auto with con res have "{E}=A" unfolding IsConnected_def 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}IsConnected" using conn_spectrum by auto } ultimately have "A{is in the spectrum of}IsConnected" by auto } then show ?thesis unfolding IsTotDis_def antiProperty_def by auto qed text{*An space is hyperconnected iff every two non-empty open sets meet.*} definition IsHConnected ("_{is hyperconnected}"90) where "T{is hyperconnected} ≡∀U V. U∈T ∧ V∈T ∧ U∩V=0 ⟶ U=0∨V=0" text{*Every hyperconnected space is connected.*} lemma HConn_imp_Conn: assumes "T{is hyperconnected}" shows "T{is connected}" proof- { fix U assume "U∈T""U {is closed in}T" then have "⋃T-U∈T""U∈T" using IsClosed_def by auto moreover have "(⋃T-U)∩U=0" by auto moreover note assms ultimately have "U=0∨(⋃T-U)=0" using IsHConnected_def by auto with `U∈T` have "U=0∨U=⋃T" by auto } then show ?thesis using IsConnected_def by auto qed lemma Indiscrete_HConn: shows "{0,X}{is hyperconnected}" unfolding IsHConnected_def by auto text{*A first example of an hyperconnected space but not indiscrete, is the cofinite topology on the natural numbers.*} lemma Cofinite_nat_HConn: assumes "¬(X≺nat)" shows "(CoFinite X){is hyperconnected}" proof- { fix U V assume "U∈(CoFinite X)""V∈(CoFinite X)""U∩V=0" then have eq:"(X-U)≺nat∨U=0""(X-V)≺nat∨V=0" unfolding Cofinite_def Cocardinal_def by auto from `U∩V=0` have un:"(X-U)∪(X-V)=X" by auto { assume AS:"(X-U)≺nat""(X-V)≺nat" from un have "X≺nat" using less_less_imp_un_less[OF AS InfCard_nat] by auto then have "False" using assms by auto } with eq(1,2) have "U=0∨V=0" by auto } then show "(CoFinite X){is hyperconnected}" using IsHConnected_def by auto qed lemma HConn_spectrum: shows "(A{is in the spectrum of}IsHConnected) ⟷ A≲1" proof assume "A{is in the spectrum of}IsHConnected" then have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is hyperconnected})" using Spec_def by auto moreover 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 ultimately have HC_Pow:"Pow(A){is hyperconnected}" by auto { assume "A=0" then have "A≲1" using empty_lepollI by auto } moreover { assume "A≠0" then obtain e where "e∈A" by blast then have "{e}∈Pow(A)" by auto moreover have "A-{e}∈Pow(A)" by auto moreover have "{e}∩(A-{e})=0" by auto moreover note HC_Pow ultimately have "A-{e}=0" unfolding IsHConnected_def by blast with `e∈A` have "A={e}" by auto 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" { fix T assume "T{is a topology}""⋃T≈A" { assume "⋃T=0" with `T{is a topology}` have "T={0}" using empty_open by auto then have "T{is hyperconnected}" unfolding IsHConnected_def by auto } moreover { assume "⋃T≠0" moreover from `A≲1``⋃T≈A` have "⋃T≲1" using eq_lepoll_trans by auto ultimately obtain E where "⋃T={E}" using lepoll_1_is_sing by blast moreover have "T⊆Pow(⋃T)" by auto ultimately have "T⊆Pow({E})" by auto then have "T⊆{0,{E}}" by blast with `T{is a topology}` have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto then have "T{is hyperconnected}" unfolding IsHConnected_def by auto } ultimately have "T{is hyperconnected}" by auto } then show "A{is in the spectrum of}IsHConnected" unfolding Spec_def by auto qed text{*In the following results we will show that anti-hyperconnectedness is a separation property between $T_1$ and $T_2$. We will show also that both implications are proper.*} text{*First, the closure of a point in every topological space is always hyperconnected. This is the reason why every anti-hyperconnected space must be $T_1$: every singleton must be closed.*} lemma (in topology0)cl_point_imp_HConn: assumes "x∈⋃T" shows "(T{restricted to}Closure({x},T)){is hyperconnected}" proof- from assms have sub:"Closure({x},T)⊆⋃T" using Top_3_L11 by auto then have tot:"⋃(T{restricted to}Closure({x},T))=Closure({x},T)" unfolding RestrictedTo_def by auto { fix A B assume AS:"A∈(T{restricted to}Closure({x},T))""B∈(T{restricted to}Closure({x},T))""A∩B=0" then have "B⊆⋃((T{restricted to}Closure({x},T)))""A⊆⋃((T{restricted to}Closure({x},T)))" by auto with tot have "B⊆Closure({x},T)""A⊆Closure({x},T)" by auto from AS(1,2) obtain UA UB where UAUB:"UA∈T""UB∈T""A=UA∩Closure({x},T)""B=UB∩Closure({x},T)" unfolding RestrictedTo_def by auto then have "Closure({x},T)-A=Closure({x},T)-(UA∩Closure({x},T))" "Closure({x},T)-B=Closure({x},T)-(UB∩Closure({x},T))" by auto then have "Closure({x},T)-A=Closure({x},T)-(UA)" "Closure({x},T)-B=Closure({x},T)-(UB)" by auto with sub have "Closure({x},T)-A=Closure({x},T)∩(⋃T-UA)" "Closure({x},T)-B=Closure({x},T)∩(⋃T-UB)" by auto moreover from UAUB have "(⋃T-UA){is closed in}T""(⋃T-UB){is closed in}T" using Top_3_L9 by auto moreover have "Closure({x},T){is closed in}T" using cl_is_closed assms by auto ultimately have "(Closure({x},T)-A){is closed in}T""(Closure({x},T)-B){is closed in}T" using Top_3_L5(1) by auto moreover { have "x∈Closure({x},T)" using cl_contains_set assms by auto moreover from AS(3) have "x∉A∨x∉B" by auto ultimately have "x∈(Closure({x},T)-A)∨x∈(Closure({x},T)-B)" by auto } ultimately have "Closure({x},T)⊆(Closure({x},T)-A) ∨ Closure({x},T)⊆(Closure({x},T)-B)" using Top_3_L13 by auto then have "A∩Closure({x},T)=0 ∨ B∩Closure({x},T)=0" by auto with `B⊆Closure({x},T)``A⊆Closure({x},T)` have "A=0∨B=0" using cl_contains_set assms by blast } then show ?thesis unfolding IsHConnected_def by auto qed text{*A consequence is that every totally-disconnected space is $T_1$.*} lemma (in topology0) tot_dis_imp_T1: assumes "T{is totally-disconnected}" shows "T{is T⇩_{1}}" proof- { fix x y assume "y∈⋃T""x∈⋃T""y≠x" then have "(T{restricted to}Closure({x},T)){is hyperconnected}" using cl_point_imp_HConn by auto then have "(T{restricted to}Closure({x},T)){is connected}" using HConn_imp_Conn by auto moreover from `x∈⋃T` have "Closure({x},T)⊆⋃T" using Top_3_L11(1) by auto moreover note assms ultimately have "Closure({x},T){is in the spectrum of}IsConnected" unfolding IsTotDis_def antiProperty_def by auto then have "Closure({x},T)≲1" using conn_spectrum by auto moreover from `x∈⋃T` have "x∈Closure({x},T)" using cl_contains_set by auto ultimately have "Closure({x},T)={x}" using lepoll_1_is_sing[of "Closure({x},T)" "x"] by auto then have "{x}{is closed in}T" using Top_3_L8 `x∈⋃T` by auto then have "⋃T-{x}∈T" unfolding IsClosed_def by auto moreover from `y∈⋃T``y≠x` have "y∈⋃T-{x}∧x∉⋃T-{x}" by auto ultimately have "∃U∈T. y∈U∧x∉U" by force } then show ?thesis unfolding isT1_def by auto qed text{*In the literature, there exists a class of spaces called sober spaces; where the only non-empty closed hyperconnected subspaces are the closures of points and closures of diferent singletons are different.*} definition IsSober ("_{is sober}"90) where "T{is sober} ≡ ∀A∈Pow(⋃T)-{0}. (A{is closed in}T ∧ ((T{restricted to}A){is hyperconnected})) ⟶ (∃x∈⋃T. A=Closure({x},T) ∧ (∀y∈⋃T. A=Closure({y},T) ⟶ y=x) )" text{*Being sober is weaker than being anti-hyperconnected.*} theorem (in topology0) anti_HConn_imp_sober: assumes "T{is anti-}IsHConnected" shows "T{is sober}" proof- { fix A assume "A∈Pow(⋃T)-{0}""A{is closed in}T""(T{restricted to}A){is hyperconnected}" with assms have "A{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto then have "A≲1" using HConn_spectrum by auto moreover with `A∈Pow(⋃T)-{0}` have "A≠0" by auto then obtain x where "x∈A" by auto ultimately have "A={x}" using lepoll_1_is_sing by auto with `A{is closed in}T` have "{x}{is closed in}T" by auto moreover from `x∈A` `A∈Pow(⋃T)-{0}` have "{x}∈Pow(⋃T)" by auto ultimately have "Closure({x},T)={x}" unfolding Closure_def ClosedCovers_def by auto with `A={x}` have "A=Closure({x},T)" by auto moreover { fix y assume "y∈⋃T""A=Closure({y},T)" then have "{y}⊆Closure({y},T)" using cl_contains_set by auto with `A=Closure({y},T)` have "y∈A" by auto with `A={x}` have "y=x" by auto } then have "∀y∈⋃T. A=Closure({y},T) ⟶ y=x" by auto moreover note `{x}∈Pow(⋃T)` ultimately have "∃x∈⋃T. A=Closure({x},T)∧(∀y∈⋃T. A=Closure({y},T) ⟶ y=x)" by auto } then show ?thesis using IsSober_def by auto qed text{*Every sober space is $T_0$.*} lemma (in topology0) sober_imp_T0: assumes "T{is sober}" shows "T{is T⇩_{0}}" proof- { fix x y assume AS:"x∈⋃T""y∈⋃T""x≠y""∀U∈T. x∈U ⟷ y∈U" from `x∈⋃T` have clx:"Closure({x},T) {is closed in}T" using cl_is_closed by auto with `x∈⋃T` have "(⋃T-Closure({x},T))∈T" using Top_3_L11(1) unfolding IsClosed_def by auto moreover from `x∈⋃T` have "x∈Closure({x},T)" using cl_contains_set by auto moreover note AS(1,4) ultimately have "y∉(⋃T-Closure({x},T))" by auto with AS(2) have "y∈Closure({x},T)" by auto with clx have ineq1:"Closure({y},T)⊆Closure({x},T)" using Top_3_L13 by auto from `y∈⋃T` have cly:"Closure({y},T) {is closed in}T" using cl_is_closed by auto with `y∈⋃T` have "(⋃T-Closure({y},T))∈T" using Top_3_L11(1) unfolding IsClosed_def by auto moreover from `y∈⋃T` have "y∈Closure({y},T)" using cl_contains_set by auto moreover note AS(2,4) ultimately have "x∉(⋃T-Closure({y},T))" by auto with AS(1) have "x∈Closure({y},T)" by auto with cly have "Closure({x},T)⊆Closure({y},T)" using Top_3_L13 by auto with ineq1 have eq:"Closure({x},T)=Closure({y},T)" by auto have "Closure({x},T)∈Pow(⋃T)-{0}" using Top_3_L11(1) `x∈⋃T` `x∈Closure({x},T)` by auto moreover note assms clx ultimately have "∃t∈⋃T.( Closure({x},T) = Closure({t}, T) ∧ (∀y∈⋃T. Closure({x},T) = Closure({y}, T) ⟶ y = t))" unfolding IsSober_def using cl_point_imp_HConn[OF `x∈⋃T`] by auto then obtain t where t_def:"t∈⋃T""Closure({x},T) = Closure({t}, T)""∀y∈⋃T. Closure({x},T) = Closure({y}, T) ⟶ y = t" by blast with eq have "y=t" using `y∈⋃T` by auto moreover from t_def `x∈⋃T` have "x=t" by blast ultimately have "y=x" by auto with `x≠y` have "False" 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 ?thesis using isT0_def by auto qed text{*Every $T_2$ space is anti-hyperconnected.*} theorem (in topology0) T2_imp_anti_HConn: assumes "T{is T⇩_{2}}" shows "T{is anti-}IsHConnected" proof- { fix TT assume "TT{is a topology}" "TT{is hyperconnected}""TT{is T⇩_{2}}" { assume "⋃TT=0" then have "⋃TT≲1" using empty_lepollI by auto then have "(⋃TT){is in the spectrum of}IsHConnected" using HConn_spectrum by auto } moreover { assume "⋃TT≠0" then obtain x where "x∈⋃TT" by blast { fix y assume "y∈⋃TT""x≠y" with `TT{is T⇩_{2}}``x∈⋃TT` obtain U V where "U∈TT""V∈TT""x∈U""y∈V""U∩V=0" unfolding isT2_def by blast with `TT{is hyperconnected}` have "False" using IsHConnected_def by auto } with `x∈⋃TT` have "⋃TT={x}" by auto then have "⋃TT≈1" using singleton_eqpoll_1 by auto then have "⋃TT≲1" using eqpoll_imp_lepoll by auto then have "(⋃TT){is in the spectrum of}IsHConnected" using HConn_spectrum by auto } ultimately have "(⋃TT){is in the spectrum of}IsHConnected" by blast } then have "∀T. ((T{is a topology}∧(T{is hyperconnected})∧(T{is T⇩_{2}}))⟶ ((⋃T){is in the spectrum of}IsHConnected))" by auto moreover note here_T2 ultimately have "∀T. T{is a topology} ⟶ ((T{is T⇩_{2}})⟶(T{is anti-}IsHConnected))" using Q_P_imp_Spec[where P=IsHConnected and Q=isT2] by auto then show ?thesis using assms topSpaceAssum by auto qed text{*Every anti-hyperconnected space is $T_1$.*} theorem anti_HConn_imp_T1: assumes "T{is anti-}IsHConnected" shows "T{is T⇩_{1}}" proof- { fix x y assume "x∈⋃T""y∈⋃T""x≠y" { assume AS:"∀U∈T. x∉U∨y∈U" from `x∈⋃T``y∈⋃T` have "{x,y}∈Pow(⋃T)" by auto then have sub:"(T{restricted to}{x,y})⊆Pow({x,y})" using RestrictedTo_def by auto { fix U V assume H:"U∈T{restricted to}{x,y}" "V∈(T{restricted to}{x,y})""U∩V=0" with AS have "x∈U⟶y∈U""x∈V⟶y∈V" unfolding RestrictedTo_def by auto with H(1,2) sub have "x∈U⟶U={x,y}""x∈V⟶V={x,y}" by auto with H sub have "x∈U⟶(U={x,y}∧V=0)""x∈V⟶(V={x,y}∧U=0)" by auto then have "(x∈U∨x∈V)⟶(U=0∨V=0)" by auto moreover from sub H have "(x∉U∧x∉V)⟶ (U=0∨V=0)" by blast ultimately have "U=0∨V=0" by auto } then have "(T{restricted to}{x,y}){is hyperconnected}" unfolding IsHConnected_def by auto with assms`{x,y}∈Pow(⋃T)` have "{x,y}{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto then have "{x,y}≲1" using HConn_spectrum 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 "∃U∈T. x∈U∧y∉U" by auto } then show ?thesis using isT1_def by auto qed text{*There is at least one topological space that is $T_1$, but not anti-hyperconnected. This space is the cofinite topology on the natural numbers.*} lemma Cofinite_not_anti_HConn: shows "¬((CoFinite nat){is anti-}IsHConnected)" and "(CoFinite nat){is T⇩_{1}}" proof- { assume "(CoFinite nat){is anti-}IsHConnected" moreover have "⋃(CoFinite nat)=nat" unfolding Cofinite_def using union_cocardinal by auto moreover have "(CoFinite nat){restricted to}nat=(CoFinite nat)" using subspace_cocardinal unfolding Cofinite_def by auto moreover have "¬(nat≺nat)" by auto then have "(CoFinite nat){is hyperconnected}" using Cofinite_nat_HConn[of "nat"] by auto ultimately have "nat{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto then have "nat≲1" using HConn_spectrum by auto moreover have "1∈nat" by auto then have "1≺nat" using n_lesspoll_nat by auto ultimately have "nat≺nat" using lesspoll_trans1 by auto then have "False" by auto } then show "¬((CoFinite nat){is anti-}IsHConnected)" by auto next show "(CoFinite nat){is T⇩_{1}}" using cocardinal_is_T1 InfCard_nat unfolding Cofinite_def by auto qed text{*The join-topology build from the cofinite topology on the natural numbers, and the excluded set topology on the natural numbers excluding @{text "{0,1}"}; is just the union of both.*} lemma join_top_cofinite_excluded_set: shows "(joinT {CoFinite nat, ExcludedSet nat {0,1}})=(CoFinite nat)∪ (ExcludedSet nat {0,1})" proof- have coftop:"(CoFinite nat){is a topology}" unfolding Cofinite_def using CoCar_is_topology InfCard_nat by auto moreover have "(ExcludedSet nat {0,1}){is a topology}" using excludedset_is_topology by auto moreover have exuni:"⋃(ExcludedSet nat {0,1})=nat" using union_excludedset by auto moreover have cofuni:"⋃(CoFinite nat)=nat" using union_cocardinal unfolding Cofinite_def by auto ultimately have "(joinT {CoFinite nat, ExcludedSet nat {0,1}}) = (THE T. (CoFinite nat)∪(ExcludedSet nat {0,1}) {is a subbase for} T)" using joinT_def by auto moreover have "⋃(CoFinite nat)∈CoFinite nat" using CoCar_is_topology[OF InfCard_nat] unfolding Cofinite_def IsATopology_def by auto with cofuni have n:"nat∈CoFinite nat" by auto have Pa:"(CoFinite nat)∪(ExcludedSet nat {0,1}) {is a subbase for}{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})}" using Top_subbase(2) by auto have "{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})}=(THE T. (CoFinite nat)∪(ExcludedSet nat {0,1}) {is a subbase for} T)" using same_subbase_same_top[where B="(CoFinite nat)∪(ExcludedSet nat {0,1})", OF _ Pa] the_equality[where a="{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})}" and P="λT. ((CoFinite nat)∪(ExcludedSet nat {0,1})){is a subbase for}T", OF Pa] by auto ultimately have equal:"(joinT {CoFinite nat, ExcludedSet nat {0,1}}) ={⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})}" by auto { fix U assume "U∈{⋃A. A∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})}" then obtain AU where "U=⋃AU" and base:"AU∈Pow({⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))})" by auto have "(CoFinite nat)⊆Pow(⋃(CoFinite nat))" by auto moreover have "(ExcludedSet nat {0,1})⊆Pow(⋃(ExcludedSet nat {0,1}))" by auto moreover note cofuni exuni ultimately have sub:"(CoFinite nat)∪(ExcludedSet nat {0,1})⊆Pow(nat)" by auto from base have "∀S∈AU. S∈{⋂B. B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))}" by blast then have "∀S∈AU. ∃B∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1})). S=⋂B" by blast then have eq:"∀S∈AU. ∃B∈Pow((CoFinite nat)∪(ExcludedSet nat {0,1})). S=⋂B" unfolding FinPow_def by blast { fix S assume "S∈AU" with eq obtain B where "B∈Pow((CoFinite nat)∪(ExcludedSet nat {0,1}))""S=⋂B" by auto with sub have "B∈Pow(Pow(nat))" by auto { fix x assume "x∈⋂B" then have "∀N∈B. x∈N""B≠0" by auto with `B∈Pow(Pow(nat))` have "x∈nat" by blast } with `S=⋂B` have "S∈Pow(nat)" by auto } then have "∀S∈AU. S∈Pow(nat)" by blast with `U=⋃AU` have "U∈Pow(nat)" by auto { assume "0∈U∨1∈U" with `U=⋃AU` obtain S where "S∈AU""0∈S∨1∈S" by auto with base obtain BS where "S=⋂BS" and bsbase:"BS∈FinPow((CoFinite nat)∪(ExcludedSet nat {0,1}))" by auto with `0∈S∨1∈S` have "∀M∈BS. 0∈M∨1∈M" by auto then have "∀M∈BS. M∉(ExcludedSet nat {0,1})-{nat}" unfolding ExcludedPoint_def ExcludedSet_def by auto moreover note bsbase n ultimately have "BS∈FinPow(CoFinite nat)" unfolding FinPow_def by auto moreover from `0∈S∨1∈S` have "S≠0" by auto with `S=⋂BS` have "BS≠0" by auto moreover note coftop ultimately have "⋂BS∈CoFinite nat" using topology0.fin_inter_open_open[OF topology0_CoCardinal[OF InfCard_nat]] unfolding Cofinite_def by auto with `S=⋂BS` have "S∈CoFinite nat" by auto with `0∈S∨1∈S` have "nat-S≺nat" unfolding Cofinite_def Cocardinal_def by auto moreover from `U=⋃AU``S∈AU` have "S⊆U" by auto then have "nat-U⊆nat-S" by auto then have "nat-U≲nat-S" using subset_imp_lepoll by auto ultimately have "nat-U≺nat" using lesspoll_trans1 by auto with `U∈Pow(nat)` have "U∈CoFinite nat" unfolding Cofinite_def Cocardinal_def by auto with `U∈Pow(nat)` have "U∈ (CoFinite nat)∪ (ExcludedSet nat {0,1})" by auto } with `U∈Pow(nat)` have "U∈(CoFinite nat)∪ (ExcludedSet nat {0,1})" unfolding ExcludedSet_def by blast } then have "({⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))})}) ⊆ (CoFinite nat)∪ (ExcludedSet nat {0,1})" by blast moreover { fix U assume "U∈(CoFinite nat)∪ (ExcludedSet nat {0,1})" then have "{U}∈FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))" unfolding FinPow_def by auto then have "{U}∈Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))})" by blast moreover have "U=⋃{U}" by auto ultimately have "U∈{⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))})}" by blast } then have "(CoFinite nat)∪ (ExcludedSet nat {0,1})⊆{⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))})}" by auto ultimately have "(CoFinite nat)∪ (ExcludedSet nat {0,1})={⋃A . A ∈ Pow({⋂B . B ∈ FinPow((CoFinite nat) ∪ (ExcludedSet nat {0,1}))})}" by auto with equal show ?thesis by auto qed text{*The previous topology in not $T_2$, but is anti-hyperconnected.*} theorem join_Cofinite_ExclPoint_not_T2: shows "¬((joinT {CoFinite nat, ExcludedSet nat {0,1}}){is T⇩_{2}})" and "(joinT {CoFinite nat, ExcludedSet nat {0,1}}){is anti-}IsHConnected" proof- have "(CoFinite nat)⊆(CoFinite nat)∪ (ExcludedSet nat {0,1})" by auto have "⋃((CoFinite nat)∪ (ExcludedSet nat {0,1}))=(⋃(CoFinite nat))∪ (⋃(ExcludedSet nat {0,1}))" by auto moreover have "…=nat "unfolding Cofinite_def using union_cocardinal union_excludedset by auto ultimately have tot:"⋃((CoFinite nat)∪ (ExcludedSet nat {0,1}))=nat" by auto { assume "(joinT {CoFinite nat, ExcludedSet nat {0, 1}}) {is T⇩_{2}}" then have t2:"((CoFinite nat)∪ (ExcludedSet nat {0,1})){is T⇩_{2}}" using join_top_cofinite_excluded_set by auto with tot have "∃U∈((CoFinite nat)∪ (ExcludedSet nat {0,1})). ∃V∈((CoFinite nat)∪ (ExcludedSet nat {0,1})). 0∈U∧1∈V∧U∩V=0" using isT2_def by auto then obtain U V where "U ∈ (CoFinite nat) ∨ (0 ∉ U∧1∉U)""V ∈ (CoFinite nat) ∨ (0 ∉ V∧1∉V)""0∈U""1∈V""U∩V=0" unfolding ExcludedSet_def by auto then have "U∈(CoFinite nat)""V∈(CoFinite nat)" by auto with `0∈U``1∈V` have "U∩V≠0" using Cofinite_nat_HConn IsHConnected_def by auto with `U∩V=0` have "False" by auto } then show "¬((joinT {CoFinite nat, ExcludedSet nat {0,1}}){is T⇩_{2}})" by auto { fix A assume AS:"A∈Pow(⋃((CoFinite nat)∪ (ExcludedSet nat {0,1})))""(((CoFinite nat)∪ (ExcludedSet nat {0,1})){restricted to}A){is hyperconnected}" with tot have "A∈Pow(nat)" by auto then have sub:"A∩nat=A" by auto have "((CoFinite nat)∪ (ExcludedSet nat {0,1})){restricted to}A=((CoFinite nat){restricted to}A)∪ ((ExcludedSet nat {0,1}){restricted to}A)" unfolding RestrictedTo_def by auto also from sub have "…=(CoFinite A)∪(ExcludedSet A {0,1})" using subspace_excludedset[of"nat""{0,1}""A"] subspace_cocardinal[of "nat""nat""A"] unfolding Cofinite_def by auto finally have "((CoFinite nat)∪ (ExcludedSet nat {0,1})){restricted to}A=(CoFinite A)∪(ExcludedSet A {0,1})" by auto with AS(2) have eq:"((CoFinite A)∪(ExcludedSet A {0,1})){is hyperconnected}" by auto { assume "{0,1}∩A=0" then have "(CoFinite A)∪(ExcludedSet A {0,1})=Pow(A)" using empty_excludedset[of "{0,1}""A"] unfolding Cofinite_def Cocardinal_def by auto with eq have "Pow(A){is hyperconnected}" by auto then have "Pow(A){is connected}" using HConn_imp_Conn by auto moreover have "Pow(A){is anti-}IsConnected" using discrete_tot_dis unfolding IsTotDis_def by auto moreover have "⋃(Pow(A))∈Pow(⋃(Pow(A)))" by auto moreover have "Pow(A){restricted to}⋃(Pow(A))=Pow(A)" unfolding RestrictedTo_def by blast ultimately have "(⋃(Pow(A))){is in the spectrum of}IsConnected" unfolding antiProperty_def by auto then have "A{is in the spectrum of}IsConnected" by auto then have "A≲1" using conn_spectrum by auto then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto } moreover { assume AS:"{0,1}∩A≠0" { assume "A={0}∨A={1}" 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}IsHConnected" using HConn_spectrum by auto } moreover { assume AS2:"¬(A={0}∨A={1})" { assume AS3:"A⊆{0,1}" with AS AS2 have A_def:"A={0,1}" by blast then have "(ExcludedSet A {0,1})=(ExcludedSet A A)" by auto moreover have "(ExcludedSet A A)={0,A}" unfolding ExcludedSet_def by blast ultimately have "(ExcludedSet A {0,1})={0,A}" by auto moreover have "0∈(CoFinite A)" using empty_open[of "CoFinite A"] CoCar_is_topology[OF InfCard_nat,of "A"] unfolding Cofinite_def by auto moreover have "⋃(CoFinite A)=A" using union_cocardinal unfolding Cofinite_def by auto then have "A∈(CoFinite A)" using CoCar_is_topology[OF InfCard_nat,of "A"] unfolding Cofinite_def IsATopology_def by auto ultimately have "(CoFinite A)∪(ExcludedSet A {0,1})=(CoFinite A)" by auto with eq have"(CoFinite A){is hyperconnected}" by auto with A_def have hyp:"(CoFinite {0,1}){is hyperconnected}" by auto have "{0}≈1""{1}≈1" using singleton_eqpoll_1 by auto moreover have "1≺nat" using n_lesspoll_nat by auto ultimately have "{0}≺nat""{1}≺nat" using eq_lesspoll_trans by auto moreover have "{0,1}-{1}={0}""{0,1}-{0}={1}" by auto ultimately have "{1}∈(CoFinite {0,1})""{0}∈(CoFinite {0,1})" "{1}∩{0}=0" unfolding Cofinite_def Cocardinal_def by auto with hyp have "False" unfolding IsHConnected_def by auto } then obtain t where "t∈A" "t≠0" "t≠1" by auto then have "{t}∈(ExcludedSet A {0,1})" unfolding ExcludedSet_def by auto moreover { have "{t}≈1" using singleton_eqpoll_1 by auto moreover have "1≺nat" using n_lesspoll_nat by auto ultimately have "{t}≺nat" using eq_lesspoll_trans by auto moreover with `t∈A` have "A-(A-{t})={t}" by auto ultimately have "A-{t}∈(CoFinite A)" unfolding Cofinite_def Cocardinal_def by auto } ultimately have "{t}∈((CoFinite A)∪(ExcludedSet A {0,1}))""A-{t}∈((CoFinite A)∪(ExcludedSet A {0,1}))" "{t}∩(A-{t})=0" by auto with eq have "A-{t}=0" unfolding IsHConnected_def by auto with `t∈A` have "A={t}" 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}IsHConnected" using HConn_spectrum by auto } ultimately have "A{is in the spectrum of}IsHConnected" by auto } ultimately have "A{is in the spectrum of}IsHConnected" by auto } then have "((CoFinite nat)∪(ExcludedSet nat {0,1})){is anti-}IsHConnected" unfolding antiProperty_def by auto then show "(joinT {CoFinite nat, ExcludedSet nat {0,1}}){is anti-}IsHConnected" using join_top_cofinite_excluded_set by auto qed text{*Let's show that anti-hyperconnected is in fact $T_1$ and sober. The trick of the proof lies in the fact that if a subset is hyperconnected, its closure is so too (the closure of a point is then always hyperconnected because singletons are in the spectrum); since the closure is closed, we can apply the sober property on it.*} theorem (in topology0) T1_sober_imp_anti_HConn: assumes "T{is T⇩_{1}}" and "T{is sober}" shows "T{is anti-}IsHConnected" proof- { fix A assume AS:"A∈Pow(⋃T)""(T{restricted to}A){is hyperconnected}" { assume "A=0" then have "A≲1" using empty_lepollI by auto then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto } moreover { assume "A≠0" then obtain x where "x∈A" by blast { assume "¬((T{restricted to}Closure(A,T)){is hyperconnected})" then obtain U V where UV_def:"U∈(T{restricted to}Closure(A,T))""V∈(T{restricted to}Closure(A,T))" "U∩V=0""U≠0""V≠0" using IsHConnected_def by auto then obtain UCA VCA where "UCA∈T""VCA∈T""U=UCA∩Closure(A,T)""V=VCA∩Closure(A,T)" unfolding RestrictedTo_def by auto from `A∈Pow(⋃T)` have "A⊆Closure(A,T)" using cl_contains_set by auto then have "UCA∩A⊆UCA∩Closure(A,T)""VCA∩A⊆VCA∩Closure(A,T)" by auto with `U=UCA∩Closure(A,T)``V=VCA∩Closure(A,T)``U∩V=0` have "(UCA∩A)∩(VCA∩A)=0" by auto moreover from `UCA∈T``VCA∈T` have "UCA∩A∈(T{restricted to}A)""VCA∩A∈(T{restricted to}A)" unfolding RestrictedTo_def by auto moreover note AS(2) ultimately have "UCA∩A=0∨VCA∩A=0" using IsHConnected_def by auto with `A⊆Closure(A,T)` have "A⊆Closure(A,T)-UCA∨A⊆Closure(A,T)-VCA" by auto moreover { have "Closure(A,T)-UCA=Closure(A,T)∩(⋃T-UCA)""Closure(A,T)-VCA=Closure(A,T)∩(⋃T-VCA)" using Top_3_L11(1) AS(1) by auto moreover with `UCA∈T``VCA∈T` have "(⋃T-UCA){is closed in}T""(⋃T-VCA){is closed in}T""Closure(A,T){is closed in}T" using Top_3_L9 cl_is_closed AS(1) by auto ultimately have "(Closure(A,T)-UCA){is closed in}T""(Closure(A,T)-VCA){is closed in}T" using Top_3_L5(1) by auto } ultimately have "Closure(A,T)⊆Closure(A,T)-UCA∨Closure(A,T)⊆Closure(A,T)-VCA" using Top_3_L13 by auto then have "UCA∩Closure(A,T)=0∨VCA∩Closure(A,T)=0" by auto with `U=UCA∩Closure(A,T)``V=VCA∩Closure(A,T)` have "U=0∨V=0" by auto with `U≠0``V≠0` have "False" by auto } then have "(T{restricted to}Closure(A,T)){is hyperconnected}" by auto moreover have "Closure(A,T){is closed in}T" using cl_is_closed AS(1) by auto moreover from `x∈A` have "Closure(A,T)≠0" using cl_contains_set AS(1) by auto moreover from AS(1) have "Closure(A,T)⊆⋃T" using Top_3_L11(1) by auto ultimately have "Closure(A,T)∈Pow(⋃T)-{0}""(T {restricted to} Closure(A, T)){is hyperconnected}" "Closure(A, T) {is closed in} T" by auto moreover note assms(2) ultimately have "∃x∈⋃T. (Closure(A,T)=Closure({x},T)∧ (∀y∈⋃T. Closure(A,T) = Closure({y}, T) ⟶ y = x))" unfolding IsSober_def by auto then obtain y where "y∈⋃T""Closure(A,T)=Closure({y},T)" by auto moreover { fix z assume "z∈(⋃T)-{y}" with assms(1) `y∈⋃T` obtain U where "U∈T" "z∈U" "y∉U" using isT1_def by blast then have "U∈T" "z∈U" "U⊆(⋃T)-{y}" by auto then have "∃U∈T. z∈U ∧ U⊆(⋃T)-{y}" by auto } then have "∀z∈(⋃T)-{y}. ∃U∈T. z∈U ∧ U⊆(⋃T)-{y}" by auto then have "⋃T-{y}∈T" using open_neigh_open by auto with `y∈⋃T` have "{y} {is closed in}T" using IsClosed_def by auto with `y∈⋃T` have "Closure({y},T)={y}" using Top_3_L8 by auto with `Closure(A,T)=Closure({y},T)` have "Closure(A,T)={y}" by auto with AS(1) have "A⊆{y}" using cl_contains_set[of "A"] by auto with `A≠0` have "A={y}" 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}IsHConnected" using HConn_spectrum by auto } ultimately have "A{is in the spectrum of}IsHConnected" by blast } then show ?thesis using antiProperty_def by auto qed theorem (in topology0) anti_HConn_iff_T1_sober: shows "(T{is anti-}IsHConnected) ⟷ (T{is sober}∧T{is T⇩_{1}})" using T1_sober_imp_anti_HConn anti_HConn_imp_T1 anti_HConn_imp_sober by auto text{*A space is ultraconnected iff every two non-empty closed sets meet.*} definition IsUConnected ("_{is ultraconnected}"80) where "T{is ultraconnected}≡ ∀A B. A{is closed in}T∧B{is closed in}T∧A∩B=0 ⟶ A=0∨B=0" text{*Every ultraconnected space is trivially normal.*} lemma (in topology0)UConn_imp_normal: assumes "T{is ultraconnected}" shows "T{is normal}" proof- { fix A B assume AS:"A{is closed in}T" "B{is closed in}T""A∩B=0" with assms have "A=0∨B=0" using IsUConnected_def by auto with AS(1,2) have "(A⊆0∧B⊆⋃T)∨(A⊆⋃T∧B⊆0)" unfolding IsClosed_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 "∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0" by auto } then show ?thesis unfolding IsNormal_def by auto qed text{*Every ultraconnected space is connected.*} lemma UConn_imp_Conn: assumes "T{is ultraconnected}" shows "T{is connected}" proof- { fix U V assume "U∈T""U{is closed in}T" then have "⋃T-(⋃T-U)=U" by auto with `U∈T` have "(⋃T-U){is closed in}T" unfolding IsClosed_def by auto with `U{is closed in}T` assms have "U=0∨⋃T-U=0" unfolding IsUConnected_def by auto with `U∈T` have "U=0∨U=⋃T" by auto } then show ?thesis unfolding IsConnected_def by auto qed lemma UConn_spectrum: shows "(A{is in the spectrum of}IsUConnected) ⟷ A≲1" proof assume A_spec:"(A{is in the spectrum of}IsUConnected)" { assume "A=0" then have "A≲1" using empty_lepollI by auto } moreover { assume "A≠0" from A_spec have "∀T. (T{is a topology}∧⋃T≈A) ⟶ (T{is ultraconnected})" unfolding Spec_def by auto moreover 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 ultimately have ult:"Pow(A){is ultraconnected}" by auto moreover from `A≠0` obtain b where "b∈A" by auto then have "{b}{is closed in}Pow(A)" unfolding IsClosed_def by auto { fix c assume "c∈A""c≠b" then have "{c}{is closed in}Pow(A)""{c}∩{b}=0" unfolding IsClosed_def by auto with ult `{b}{is closed in}Pow(A)` have "False" using IsUConnected_def by auto } with `b∈A` have "A={b}" by auto 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" { fix T assume "T{is a topology}""⋃T≈A" { assume "⋃T=0" with `T{is a topology}` have "T={0}" using empty_open by auto then have "T{is ultraconnected}" unfolding IsUConnected_def IsClosed_def by auto } moreover { assume "⋃T≠0" moreover from `A≲1``⋃T≈A` have "⋃T≲1" using eq_lepoll_trans by auto ultimately obtain E where eq:"⋃T={E}" using lepoll_1_is_sing by blast moreover have "T⊆Pow(⋃T)" by auto ultimately have "T⊆Pow({E})" by auto then have "T⊆{0,{E}}" by blast with `T{is a topology}` have "{0}⊆T" "T⊆{0,{E}}" using empty_open by auto then have "T{is ultraconnected}" unfolding IsUConnected_def IsClosed_def by (simp only: eq, safe, force) } ultimately have "T{is ultraconnected}" by auto } then show "A{is in the spectrum of}IsUConnected" unfolding Spec_def by auto qed text{*This time, anti-ultraconnected is an old property.*} theorem (in topology0) anti_UConn: shows "(T{is anti-}IsUConnected) ⟷ T{is T⇩_{1}}" proof assume "T{is T⇩_{1}}" { fix TT { assume "TT{is a topology}""TT{is T⇩_{1}}""TT{is ultraconnected}" { assume "⋃TT=0" then have "⋃TT≲1" using empty_lepollI by auto then have "((⋃TT){is in the spectrum of}IsUConnected)" using UConn_spectrum by auto } moreover { assume "⋃TT≠0" then obtain t where "t∈⋃TT" by blast { fix x assume p:"x∈⋃TT" { fix y assume "y∈(⋃TT)-{x}" with `TT{is T⇩_{1}}` p obtain U where "U∈TT" "y∈U" "x∉U" using isT1_def by blast then have "U∈TT" "y∈U" "U⊆(⋃TT)-{x}" by auto then have "∃U∈TT. y∈U ∧ U⊆(⋃TT)-{x}" by auto } then have "∀y∈(⋃TT)-{x}. ∃U∈TT. y∈U ∧ U⊆(⋃TT)-{x}" by auto with `TT{is a topology}` have "⋃TT-{x}∈TT" using topology0.open_neigh_open unfolding topology0_def by auto with p have "{x} {is closed in}TT" using IsClosed_def by auto } then have reg:"∀x∈⋃TT. {x}{is closed in}TT" by auto with `t∈⋃TT` have t_cl:"{t}{is closed in}TT" by auto { fix y assume "y∈⋃TT" with reg have "{y}{is closed in}TT" by auto with `TT{is ultraconnected}` t_cl have "y=t" unfolding IsUConnected_def by auto } with `t∈⋃TT` have "⋃TT={t}" by blast then have "⋃TT≈1" using singleton_eqpoll_1 by auto then have "⋃TT≲1" using eqpoll_imp_lepoll by auto then have "(⋃TT){is in the spectrum of}IsUConnected" using UConn_spectrum by auto } ultimately have "(⋃TT){is in the spectrum of}IsUConnected" by blast } then have "(TT{is a topology}∧TT{is T⇩_{1}}∧(TT{is ultraconnected}))⟶ ((⋃TT){is in the spectrum of}IsUConnected)" by auto } then have "∀TT. (TT{is a topology}∧TT{is T⇩_{1}}∧(TT{is ultraconnected}))⟶ ((⋃TT){is in the spectrum of}IsUConnected)" by auto moreover note here_T1 ultimately have "∀T. T{is a topology} ⟶ ((T{is T⇩_{1}})⟶(T{is anti-}IsUConnected))" using Q_P_imp_Spec[where Q=isT1 and P=IsUConnected] by auto with topSpaceAssum have "(T{is T⇩_{1}})⟶(T{is anti-}IsUConnected)" by auto with `T{is T⇩_{1}}` show "T{is anti-}IsUConnected" by auto next assume ASS:"T{is anti-}IsUConnected" { fix x y assume "x∈⋃T""y∈⋃T""x≠y" then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto { assume AS:"∀U∈T. x∈U⟶y∈U" { assume "{y}{is closed in}(T{restricted to}{x,y})" moreover from `x≠y` have "{x,y}-{y}={x}" by auto ultimately have "{x}∈(T{restricted to}{x,y})" unfolding IsClosed_def by (simp only:tot) then obtain U where "U∈T""{x}={x,y}∩U" unfolding RestrictedTo_def by auto moreover with `x≠y` have "y∉{x}" "y∈{x,y}" by (blast+) with `{x}={x,y}∩U` have "y∉U" by auto moreover have "x∈{x}" by auto with `{x}={x,y}∩U` have "x∈U" by auto ultimately have "x∈U""y∉U""U∈T" by auto with AS have "False" by auto } then have y_no_cl:"¬({y}{is closed in}(T{restricted to}{x,y}))" by auto { fix A B assume cl:"A{is closed in}(T{restricted to}{x,y})""B{is closed in}(T{restricted to}{x,y})""A∩B=0" with tot have "A⊆{x,y}""B⊆{x,y}""A∩B=0" unfolding IsClosed_def by auto then have "x∈A⟶x∉B""y∈A⟶y∉B""A⊆{x,y}""B⊆{x,y}" by auto { assume "x∈A" with `x∈A⟶x∉B``B⊆{x,y}` have "B⊆{y}" by auto then have "B=0∨B={y}" by auto with y_no_cl cl(2) have "B=0" by auto } moreover { assume "x∉A" with `A⊆{x,y}` have "A⊆{y}" by auto then have "A=0∨A={y}" by auto with y_no_cl cl(1) have "A=0" by auto } ultimately have "A=0∨B=0" by auto } then have "(T{restricted to}{x,y}){is ultraconnected}" unfolding IsUConnected_def by auto with ASS `x∈⋃T``y∈⋃T` have "{x,y}{is in the spectrum of}IsUConnected" unfolding antiProperty_def by auto then have "{x,y}≲1" using UConn_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 "y=x" by auto then have "False" using `x≠y` by auto } then have "∃U∈T. x∈U∧y∉U" by auto } then show "T{is T⇩_{1}}" unfolding isT1_def by auto qed text{*Is is natural that separation axioms and connection axioms are anti-properties of each other; as the concepts of connectedness and separation are opposite.*} text{*To end this section, let's try to charaterize anti-sober spaces.*} lemma sober_spectrum: shows "(A{is in the spectrum of}IsSober) ⟷ A≲1" proof assume AS:"A{is in the spectrum of}IsSober" { assume "A=0" then have "A≲1" using empty_lepollI by auto } moreover { assume "A≠0" note AS moreover have top:"{0,A}{is a topology}" unfolding IsATopology_def by auto moreover have "⋃{0,A}=A" by auto then have "⋃{0,A}≈A" by auto ultimately have "{0,A}{is sober}" using Spec_def by auto moreover have "{0,A}{is hyperconnected}" using Indiscrete_HConn by auto moreover have "{0,A}{restricted to}A={0,A}" unfolding RestrictedTo_def by auto moreover have "A{is closed in}{0,A}" unfolding IsClosed_def by auto moreover note `A≠0` ultimately have "∃x∈A. A=Closure({x},{0,A})∧ (∀y∈⋃{0, A}. A = Closure({y}, {0, A}) ⟶ y = x)" unfolding IsSober_def by auto then obtain x where "x∈A" "A=Closure({x},{0,A})" and reg:"∀y∈A. A = Closure({y}, {0, A}) ⟶ y = x" by auto { fix y assume "y∈A" with top have "Closure({y},{0,A}){is closed in}{0,A}" using topology0.cl_is_closed topology0_def by auto moreover from `y∈A` top have "y∈Closure({y},{0,A})" using topology0.cl_contains_set topology0_def by auto ultimately have "A-Closure({y},{0,A})∈{0,A}""Closure({y},{0,A})∩A≠0" unfolding IsClosed_def by auto then have "A-Closure({y},{0,A})=A∨A-Closure({y},{0,A})=0" by auto moreover from `y∈A``y∈Closure({y},{0,A})` have "y∈A""y∉A-Closure({y},{0,A})" by auto ultimately have "A-Closure({y},{0,A})=0" by (cases "A-Closure({y},{0,A})=A", simp, auto) moreover from `y∈A` top have "Closure({y},{0,A})⊆A" using topology0_def topology0.Top_3_L11(1) by blast then have "A-(A-Closure({y},{0,A}))=Closure({y},{0,A})" by auto ultimately have "A=Closure({y},{0,A})" by auto } with reg have "∀y∈A. x=y" 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 } ultimately show "A≲1" by auto next assume "A≲1" { fix T assume "T{is a topology}""⋃T≈A" { assume "⋃T=0" then have "T{is sober}" unfolding IsSober_def by auto } moreover { assume "⋃T≠0" then obtain x where "x∈⋃T" by blast moreover from `⋃T≈A` `A≲1` have "⋃T≲1" using eq_lepoll_trans by auto ultimately have "⋃T={x}" using lepoll_1_is_sing by auto moreover have "T⊆Pow(⋃T)" by auto ultimately have "T⊆Pow({x})" by auto then have "T⊆{0,{x}}" by blast moreover from `T{is a topology}` have "0∈T" using empty_open by auto moreover from `T{is a topology}` have "⋃T∈T" unfolding IsATopology_def by auto with `⋃T={x}` have "{x}∈T" by auto ultimately have T_def:"T={0,{x}}" by auto then have dd:"Pow(⋃T)-{0}={{x}}" by auto { fix B assume "B∈Pow(⋃T)-{0}" with dd have B_def:"B={x}" by auto from `T{is a topology}` have "(⋃T){is closed in}T" using topology0_def topology0.Top_3_L1 by auto with `⋃T={x}` `T{is a topology}` have "Closure({x},T)={x}" using topology0.Top_3_L8 unfolding topology0_def by auto with B_def have "B=Closure({x},T)" by auto moreover { fix y assume "y∈⋃T" with `⋃T={x}` have "y=x" by auto } then have "(∀y∈⋃T. B = Closure({y}, T) ⟶ y = x)" by auto moreover note `x∈⋃T` ultimately have "(∃x∈⋃T. B = Closure({x}, T) ∧ (∀y∈⋃T. B = Closure({y}, T) ⟶ y = x))" by auto } then have "T{is sober}" unfolding IsSober_def by auto } ultimately have "T{is sober}" by blast } then show "A {is in the spectrum of} IsSober" unfolding Spec_def by auto qed theorem (in topology0)anti_sober: shows "(T{is anti-}IsSober) ⟷ T={0,⋃T}" proof assume "T={0,⋃T}" { fix A assume "A∈Pow(⋃T)""(T{restricted to}A){is sober}" { assume "A=0" then have "A≲1" using empty_lepollI by auto then have "A{is in the spectrum of}IsSober" using sober_spectrum by auto } moreover { assume "A≠0" have "⋃T∈{0,⋃T}""0∈{0,⋃T}" by auto with `T={0,⋃T}` have "(⋃T)∈T" "0∈T" by auto with `A∈Pow(⋃T)` have "{0,A}⊆(T{restricted to}A)" unfolding RestrictedTo_def by auto moreover have "∀B∈{0,⋃T}. B=0∨B=⋃T" by auto with `T={0,⋃T}` have "∀B∈T. B=0∨B=⋃T" by auto with `A∈Pow(⋃T)` have "T{restricted to}A⊆{0,A}" unfolding RestrictedTo_def by auto ultimately have top_def:"T{restricted to}A={0,A}" by auto moreover have "A{is closed in}{0,A}" unfolding IsClosed_def by auto moreover have "{0,A}{is hyperconnected}" using Indiscrete_HConn by auto moreover from `A∈Pow(⋃T)` have "(T{restricted to}A){restricted to}A=T{restricted to}A" using subspace_of_subspace[of "A""A""T"] by auto moreover note `A≠0` `A∈Pow(⋃T)` ultimately have "A∈Pow(⋃(T{restricted to}A))-{0}""A{is closed in}(T{restricted to}A)""((T{restricted to}A){restricted to}A){is hyperconnected}" by auto with `(T{restricted to}A){is sober}` have "∃x∈⋃(T{restricted to}A). A=Closure({x},T{restricted to}A)∧(∀y∈⋃(T{restricted to}A). A=Closure({y},T{restricted to}A) ⟶ y=x)" unfolding IsSober_def by auto with top_def have "∃x∈A. A=Closure({x},{0,A})∧(∀y∈A. A=Closure({y},{0,A}) ⟶ y=x)" by auto then obtain x where "x∈A""A=Closure({x},{0,A})"and reg:"∀y∈A. A=Closure({y},{0,A}) ⟶ y=x" by auto { fix y assume "y∈A" from `A≠0` have top:"{0,A}{is a topology}" using indiscrete_ptopology[of "A"] indiscrete_partition[of "A"] Ptopology_is_a_topology(1)[of "{A}""A"] by auto with `y∈A` have "Closure({y},{0,A}){is closed in}{0,A}" using topology0.cl_is_closed topology0_def by auto moreover from `y∈A` top have "y∈Closure({y},{0,A})" using topology0.cl_contains_set topology0_def by auto ultimately have "A-Closure({y},{0,A})∈{0,A}""Closure({y},{0,A})∩A≠0" unfolding IsClosed_def by auto then have "A-Closure({y},{0,A})=A∨A-Closure({y},{0,A})=0" by auto moreover from `y∈A``y∈Closure({y},{0,A})` have "y∈A""y∉A-Closure({y},{0,A})" by auto ultimately have "A-Closure({y},{0,A})=0" by (cases "A-Closure({y},{0,A})=A", simp, auto) moreover from `y∈A` top have "Closure({y},{0,A})⊆A" using topology0_def topology0.Top_3_L11(1) by blast then have "A-(A-Closure({y},{0,A}))=Closure({y},{0,A})" by auto ultimately have "A=Closure({y},{0,A})" by auto } with reg `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}IsSober" using sober_spectrum by auto } ultimately have "A{is in the spectrum of}IsSober" by auto } then show "T{is anti-}IsSober" using antiProperty_def by auto next assume "T{is anti-}IsSober" { fix A assume "A∈T""A≠0""A≠⋃T" then obtain x y where "x∈A""y∈⋃T-A" "x≠y"by blast then have "{x}={x,y}∩A" by auto with `A∈T` have "{x}∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto { assume "{y}∈T{restricted to}{x,y}" from `y∈⋃T-A` `x∈A``A∈T` have "⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto with `x≠y``{y}∈T{restricted to}{x,y}``{x}∈T{restricted to}{x,y}` have "(T{restricted to}{x,y}){is T⇩_{2}}" unfolding isT2_def by auto then have "(T{restricted to}{x,y}){is sober}" using topology0.T2_imp_anti_HConn[of "T{restricted to}{x,y}"] Top_1_L4 topology0_def topology0.anti_HConn_iff_T1_sober[of "T{restricted to}{x,y}"] by auto } moreover { assume "{y}∉T{restricted to}{x,y}" moreover from `y∈⋃T-A` `x∈A``A∈T` have "T{restricted to}{x,y}⊆Pow({x,y})" unfolding RestrictedTo_def by auto then have "T{restricted to}{x,y}⊆{0,{x},{y},{x,y}}" by blast moreover note `{x}∈T{restricted to}{x,y}` empty_open[OF Top_1_L4[of "{x,y}"]] moreover from `y∈⋃T-A` `x∈A``A∈T` have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto from Top_1_L4[of "{x,y}"] have "⋃(T{restricted to}{x,y})∈T{restricted to}{x,y}" unfolding IsATopology_def by auto with tot have "{x,y}∈T{restricted to}{x,y}" by auto ultimately have top_d_def:"T{restricted to}{x,y}={0,{x},{x,y}}" by auto { fix B assume "B∈Pow({x,y})-{0}""B{is closed in}(T{restricted to}{x,y})" with top_d_def have "(⋃(T{restricted to}{x,y}))-B∈{0,{x},{x,y}}" unfolding IsClosed_def by simp moreover have "B∈{{x},{y},{x,y}}" using `B∈Pow({x,y})-{0}` by blast moreover note tot ultimately have "{x,y}-B∈{0,{x},{x,y}}" by auto have xin:"x∈Closure({x},T{restricted to}{x,y})" using topology0.cl_contains_set[of "T{restricted to}{x,y}""{x}"] Top_1_L4[of "{x,y}"] unfolding topology0_def[of "(T {restricted to} {x, y})"] using tot by auto { assume "{x}{is closed in}(T{restricted to}{x,y})" then have "{x,y}-{x}∈(T{restricted to}{x,y})" unfolding IsClosed_def using tot by auto moreover from `x≠y` have "{x,y}-{x}={y}" by auto ultimately have "{y}∈(T{restricted to}{x,y})" by auto then have "False" using `{y}∉(T{restricted to}{x,y})` by auto } then have "¬({x}{is closed in}(T{restricted to}{x,y}))" by auto moreover from tot have "(Closure({x},T{restricted to}{x,y})){is closed in}(T{restricted to}{x,y})" using topology0.cl_is_closed unfolding topology0_def using Top_1_L4[of "{x,y}"] tot by auto ultimately have "¬(Closure({x},T{restricted to}{x,y})={x})" by auto moreover note xin topology0.Top_3_L11(1)[of "T{restricted to}{x,y}""{x}"] tot ultimately have cl_x:"Closure({x},T{restricted to}{x,y})={x,y}" unfolding topology0_def using Top_1_L4[of "{x,y}"] by auto have "{y}{is closed in}(T{restricted to}{x,y})" unfolding IsClosed_def using tot top_d_def `x≠y` by auto then have cl_y:"Closure({y},T{restricted to}{x,y})={y}" using topology0.Top_3_L8[of "T{restricted to}{x,y}"] unfolding topology0_def using Top_1_L4[of "{x,y}"] tot by auto { assume "{x,y}-B=0" with `B∈Pow({x,y})-{0}` have B:"{x,y}=B" by auto { fix m assume dis:"m∈{x,y}" and B_def:"B=Closure({m},T{restricted to}{x,y})" { assume "m=y" with B_def have "B=Closure({y},T{restricted to}{x,y})" by auto with cl_y have "B={y}" by auto with B have "{x,y}={y}" by auto moreover have "x∈{x,y}" by auto ultimately have "x∈{y}" by auto with `x≠y` have "False" by auto } with dis have "m=x" by auto } then have "(∀m∈{x,y}. B=Closure({m},T{restricted to}{x,y})⟶m=x )" by auto moreover have "B=Closure({x},T{restricted to}{x,y})" using cl_x B by auto ultimately have "∃t∈{x,y}. B=Closure({t},T{restricted to}{x,y}) ∧ (∀m∈{x,y}. B=Closure({m},T{restricted to}{x,y})⟶m=t )" by auto } moreover { assume "{x,y}-B≠0" with `{x,y}-B∈{0,{x},{x,y}}` have or:"{x,y}-B={x}∨{x,y}-B={x,y}" by auto { assume "{x,y}-B={x}" then have "x∈{x,y}-B" by auto with `B∈{{x},{y},{x,y}}` `x≠y` have B:"B={y}" by blast { fix m assume dis:"m∈{x,y}" and B_def:"B=Closure({m},T{restricted to}{x,y})" { assume "m=x" with B_def have "B=Closure({x},T{restricted to}{x,y})" by auto with cl_x have "B={x,y}" by auto with B have "{x,y}={y}" by auto moreover have "x∈{x,y}" by auto ultimately have "x∈{y}" by auto with `x≠y` have "False" by auto } with dis have "m=y" by auto } moreover have "B=Closure({y},T{restricted to}{x,y})" using cl_y B by auto ultimately have "∃t∈{x,y}. B=Closure({t},T{restricted to}{x,y}) ∧ (∀m∈{x,y}. B=Closure({m},T{restricted to}{x,y})⟶m=t )" by auto } moreover { assume "{x,y}-B≠{x}" with or have "{x,y}-B={x,y}" by auto then have "x∈{x,y}-B""y∈{x,y}-B" by auto with `B∈{{x},{y},{x,y}}` `x≠y` have "False" by auto } ultimately have "∃t∈{x,y}. B=Closure({t},T{restricted to}{x,y}) ∧ (∀m∈{x,y}. B=Closure({m},T{restricted to}{x,y})⟶m=t )" by auto } ultimately have "∃t∈{x,y}. B=Closure({t},T{restricted to}{x,y}) ∧ (∀m∈{x,y}. B=Closure({m},T{restricted to}{x,y})⟶m=t )" by auto } then have "(T{restricted to}{x,y}){is sober}" unfolding IsSober_def using tot by auto } ultimately have "(T{restricted to}{x,y}){is sober}" by auto with `T{is anti-}IsSober` have "{x,y}{is in the spectrum of}IsSober" unfolding antiProperty_def using `x∈A``A∈T``y∈⋃T-A` by auto then have "{x,y}≲1" using sober_spectrum 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 "False" using `x≠y` by auto } then have "T⊆{0,⋃T}" by auto with empty_open[OF topSpaceAssum] topSpaceAssum show "T={0,⋃T}" unfolding IsATopology_def by auto qed end