imports Topology_ZF_1b Topology_ZF_11

(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Properties in topology 2› theory Topology_ZF_properties_2 imports Topology_ZF_7 Topology_ZF_1b Finite_ZF_1 Topology_ZF_11 begin subsection{*Local properties.*} text{*This theory file deals with local topological properties; and applies local compactness to the one point compactification.*} text{*We will say that a topological space is locally @term{"P"} iff every point has a neighbourhood basis of subsets that have the property @term{"P"} as subspaces.*} definition IsLocally ("_{is locally}_" 90) where "T{is a topology} ⟹ T{is locally}P ≡ (∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,T) ∧ P(c,T)))" subsection{*First examples*} text{*Our first examples deal with the locally finite property. Finiteness is a property of sets, and hence it is preserved by homeomorphisms; which are in particular bijective.*} text{*The discrete topology is locally finite.*} lemma discrete_locally_finite: shows "Pow(A){is locally}(λA.(λB. Finite(A)))" proof- have "∀b∈Pow(A). ⋃(Pow(A){restricted to}b)=b" unfolding RestrictedTo_def by blast then have "∀b∈{{x}. x∈A}. Finite(b)" by auto moreover have reg:"∀S∈Pow(A). Interior(S,Pow(A))=S" unfolding Interior_def by auto { fix x b assume "x∈⋃Pow(A)" "b∈Pow(A)" "x∈b" then have "{x}⊆b" "x∈Interior({x},Pow(A))" "Finite({x})" using reg by auto then have "∃c∈Pow(b). x∈Interior(c,Pow(A))∧Finite(c)" by blast } then have "∀x∈⋃Pow(A). ∀b∈Pow(A). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,Pow(A)) ∧ Finite(c))" by auto then show ?thesis using IsLocally_def[OF Pow_is_top] by auto qed text{*The included set topology is locally finite when the set is finite.*} lemma included_finite_locally_finite: assumes "Finite(A)" and "A⊆X" shows "(IncludedSet X A){is locally}(λA.(λB. Finite(A)))" proof- have "∀b∈Pow(X). b∩A⊆b" by auto moreover note assms(1) ultimately have rr:"∀b∈{A∪{x}. x∈X}. Finite(b)" by force { fix x b assume "x∈⋃(IncludedSet X A)" "b∈(IncludedSet X A)" "x∈b" then have "A∪{x}⊆b" "A∪{x}∈{A∪{x}. x∈X}" and sub: "b⊆X" unfolding IncludedSet_def by auto moreover have "A ∪ {x} ⊆ X" using assms(2) sub `x∈b` by auto then have "x∈Interior(A∪{x},IncludedSet X A)" using interior_set_includedset[of "A∪{x}""X""A"] by auto ultimately have "∃c∈Pow(b). x∈Interior(c,IncludedSet X A)∧ Finite(c)" using rr by blast } then have "∀x∈⋃(IncludedSet X A). ∀b∈(IncludedSet X A). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,IncludedSet X A)∧ Finite(c))" by auto then show ?thesis using IsLocally_def includedset_is_topology by auto qed subsection{*Local compactness*} definition IsLocallyComp ("_{is locally-compact}" 70) where "T{is locally-compact}≡T{is locally}(λB. λT. B{is compact in}T)" text{*We center ourselves in local compactness, because it is a very important tool in topological groups and compactifications.*} text{*If a subset is compact of some cardinal for a topological space, it is compact of the same cardinal in the subspace topology.*} lemma compact_imp_compact_subspace: assumes "A{is compact of cardinal}K{in}T" "A⊆B" shows "A{is compact of cardinal}K{in}(T{restricted to}B)" unfolding IsCompactOfCard_def proof from assms show C:"Card(K)" unfolding IsCompactOfCard_def by auto from assms have "A⊆⋃T" unfolding IsCompactOfCard_def by auto then have AA:"A⊆⋃(T{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto moreover { fix M assume "M∈Pow(T{restricted to}B)" "A⊆⋃M" let ?M="{S∈T. B∩S∈M}" from `M∈Pow(T{restricted to}B)` have "⋃M⊆⋃?M" unfolding RestrictedTo_def by auto with `A⊆⋃M` have "A⊆⋃?M""?M∈Pow(T)" by auto with assms have "∃N∈Pow(?M). A⊆⋃N∧N≺K" unfolding IsCompactOfCard_def by auto then obtain N where "N∈Pow(?M)" "A⊆⋃N" "N≺K" by auto then have "N{restricted to}B⊆M" unfolding RestrictedTo_def FinPow_def by auto moreover let ?f="{⟨𝔅,B∩𝔅⟩. 𝔅∈N}" have "?f:N→(N{restricted to}B)" unfolding Pi_def function_def domain_def RestrictedTo_def by auto then have "?f∈surj(N,N{restricted to}B)" unfolding surj_def RestrictedTo_def using apply_equality by auto from `N≺K` have "N≲K" unfolding lesspoll_def by auto with `?f∈surj(N,N{restricted to}B)` have "N{restricted to}B≲N" using surj_fun_inv_2 Card_is_Ord C by auto with `N≺K` have "N{restricted to}B≺K" using lesspoll_trans1 by auto moreover from `A⊆⋃N` have "A⊆⋃(N{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto ultimately have "∃N∈Pow(M). A⊆⋃N ∧ N≺K" by auto } with AA show "A ⊆ ⋃(T {restricted to} B) ∧ (∀M∈Pow(T {restricted to} B). A ⊆ ⋃M ⟶ (∃N∈Pow(M). A ⊆ ⋃N ∧ N≺K))" by auto qed text{*The converse of the previous result is not always true. For compactness, it holds because the axiom of finite choice always holds.*} lemma compact_subspace_imp_compact: assumes "A{is compact in}(T{restricted to}B)" "A⊆B" shows "A{is compact in}T" unfolding IsCompact_def proof from assms show "A⊆⋃T" unfolding IsCompact_def RestrictedTo_def by auto next { fix M assume "M∈Pow(T)" "A⊆⋃M" let ?M="M{restricted to}B" from `M∈Pow(T)` have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto from `A⊆⋃M` have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto with assms `?M∈Pow(T{restricted to}B)` obtain N where "N∈FinPow(?M)" "A⊆⋃N" unfolding IsCompact_def by blast from `N∈FinPow(?M)` have "N≺nat" unfolding FinPow_def Finite_def using n_lesspoll_nat eq_lesspoll_trans by auto then have "Finite(N)" using lesspoll_nat_is_Finite 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 moreover { fix BB assume "BB∈N" with `N∈FinPow(?M)` have "BB∈?M" unfolding FinPow_def by auto then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto then have "S∈{S∈M. B∩S=BB}" by auto then obtain "{S∈M. B∩S=BB}≠0" by auto } then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover from `n∈nat` have " (N ≲ n ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))" using finite_choice unfolding AxiomCardinalChoiceGen_def by blast ultimately obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto then have "{f`t. t∈N}⊆M" by auto { fix t assume "t∈N" with ss have "f`t∈{S∈M. B∩S∈N}" by auto } with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover { fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb" from AAA(1) ss have "B∩ (f`aa) =aa" by auto with AAA(3) have "B∩(f`bb)=aa" by auto with ss AAA(2) have "aa=bb" by auto } ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto then have "f∈bij(N,range(f))" using inj_bij_range by auto then have "f∈bij(N,f``N)" using range_image_domain FF by auto then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto with `N≈n` have "{f`t. t∈N}≈n" using eqpoll_sym eqpoll_trans by blast with `n∈nat` have "Finite({f`t. t∈N})" unfolding Finite_def by auto with ss have "{f`t. t∈N}∈FinPow(M)" unfolding FinPow_def by auto moreover { fix aa assume "aa∈A" with `A⊆⋃N` obtain b where "b∈N" and "aa∈b" by auto with ss have "B∩(f`b)=b" by auto with `aa∈b` have "aa∈B∩(f`b)" by auto then have "aa∈ f`b" by auto with `b∈N` have "aa∈⋃{f`t. t∈N}" by auto } then have "A⊆⋃{f`t. t∈N}" by auto ultimately have "∃R∈FinPow(M). A⊆⋃R" by auto } then show "∀M∈Pow(T). A ⊆ ⋃M ⟶ (∃N∈FinPow(M). A ⊆ ⋃N)" by auto qed text{*If the axiom of choice holds for some cardinal, then we can drop the compact sets of that cardial are compact of the same cardinal as subspaces of every superspace.*} lemma Kcompact_subspace_imp_Kcompact: assumes "A{is compact of cardinal}Q{in}(T{restricted to}B)" "A⊆B" "({the axiom of} Q {choice holds})" shows "A{is compact of cardinal}Q{in}T" proof - from assms(1) have a1:"Card(Q)" unfolding IsCompactOfCard_def RestrictedTo_def by auto from assms(1) have a2:"A⊆⋃T" unfolding IsCompactOfCard_def RestrictedTo_def by auto { fix M assume "M∈Pow(T)" "A⊆⋃M" let ?M="M{restricted to}B" from `M∈Pow(T)` have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto from `A⊆⋃M` have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto with assms `?M∈Pow(T{restricted to}B)` obtain N where N:"N∈Pow(?M)" "A⊆⋃N" "N ≺ Q" unfolding IsCompactOfCard_def by blast from N(3) have "N≲Q" using lesspoll_imp_lepoll by auto moreover { fix BB assume "BB∈N" with `N∈Pow(?M)` have "BB∈?M" unfolding FinPow_def by auto then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto then have "S∈{S∈M. B∩S=BB}" by auto then obtain "{S∈M. B∩S=BB}≠0" by auto } then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover have " (N ≲ Q ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))" using assms(3) unfolding AxiomCardinalChoiceGen_def by blast ultimately obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto then have "{f`t. t∈N}⊆M" by auto { fix t assume "t∈N" with ss have "f`t∈{S∈M. B∩S∈N}" by auto } with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover { fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb" from AAA(1) ss have "B∩ (f`aa) =aa" by auto with AAA(3) have "B∩(f`bb)=aa" by auto with ss AAA(2) have "aa=bb" by auto } ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto then have "f∈bij(N,range(f))" using inj_bij_range by auto then have "f∈bij(N,f``N)" using range_image_domain FF by auto then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto with `N≺Q` have "{f`t. t∈N}≺Q" using eqpoll_sym eq_lesspoll_trans by blast moreover with ss have "{f`t. t∈N}∈Pow(M)" unfolding FinPow_def by auto moreover { fix aa assume "aa∈A" with `A⊆⋃N` obtain b where "b∈N" and "aa∈b" by auto with ss have "B∩(f`b)=b" by auto with `aa∈b` have "aa∈B∩(f`b)" by auto then have "aa∈ f`b" by auto with `b∈N` have "aa∈⋃{f`t. t∈N}" by auto } then have "A⊆⋃{f`t. t∈N}" by auto ultimately have "∃R∈Pow(M). A⊆⋃R ∧ R≺Q" by auto } then show ?thesis using a1 a2 unfolding IsCompactOfCard_def by auto qed text{*Every set, with the cofinite topology is compact.*} lemma cofinite_compact: shows "X {is compact in}(CoFinite X)" unfolding IsCompact_def proof show "X⊆⋃(CoFinite X)" using union_cocardinal unfolding Cofinite_def by auto next { fix M assume "M∈Pow(CoFinite X)" "X⊆⋃M" { assume "M=0∨M={0}" then have "M∈FinPow(M)" unfolding FinPow_def by auto with `X⊆⋃M` have "∃N∈FinPow(M). X⊆⋃N" by auto } moreover { assume "M≠0""M≠{0}" then obtain U where "U∈M""U≠0" by auto with `M∈Pow(CoFinite X)` have "U∈CoFinite X" by auto with `U≠0` have "U⊆X" "(X-U)≺nat" unfolding Cofinite_def Cocardinal_def by auto then have "Finite(X-U)" using lesspoll_nat_is_Finite by auto then have "(X-U){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto then have "((⋃(CoFinite (X-U)))≈X-U) ⟶ ((⋃(CoFinite (X-U))){is compact in}(CoFinite (X-U)))" unfolding Spec_def using InfCard_nat CoCar_is_topology unfolding Cofinite_def by auto then have com:"(X-U){is compact in}(CoFinite (X-U))" using union_cocardinal unfolding Cofinite_def by auto have "(X-U)∩X=X-U" by auto then have "(CoFinite X){restricted to}(X-U)=(CoFinite (X-U))" using subspace_cocardinal unfolding Cofinite_def by auto with com have "(X-U){is compact in}(CoFinite X)" using compact_subspace_imp_compact[of "X-U""CoFinite X""X-U"] by auto moreover have "X-U⊆⋃M" using `X⊆⋃M` by auto moreover note `M∈Pow(CoFinite X)` ultimately have "∃N∈FinPow(M). X-U⊆⋃N" unfolding IsCompact_def by auto then obtain N where "N⊆M" "Finite(N)" "X-U⊆⋃N" unfolding FinPow_def by auto with `U∈M` have "N ∪{U}⊆M" "Finite(N ∪{U})" "X⊆⋃(N ∪{U})" by auto then have "∃N∈FinPow(M). X⊆⋃N" unfolding FinPow_def by blast } ultimately have "∃N∈FinPow(M). X⊆⋃N" by auto } then show "∀M∈Pow(CoFinite X). X ⊆ ⋃M ⟶ (∃N∈FinPow(M). X ⊆ ⋃N)" by auto qed text{*A corollary is then that the cofinite topology is locally compact; since every subspace of a cofinite space is cofinite.*} corollary cofinite_locally_compact: shows "(CoFinite X){is locally-compact}" proof- have cof:"topology0(CoFinite X)" and cof1:"(CoFinite X){is a topology}" using CoCar_is_topology InfCard_nat Cofinite_def unfolding topology0_def by auto { fix x B assume "x∈⋃(CoFinite X)" "B∈(CoFinite X)" "x∈B" then have "x∈Interior(B,CoFinite X)" using topology0.Top_2_L3[OF cof] by auto moreover from `B∈(CoFinite X)` have "B⊆X" unfolding Cofinite_def Cocardinal_def by auto then have "B∩X=B" by auto then have "(CoFinite X){restricted to}B=CoFinite B" using subspace_cocardinal unfolding Cofinite_def by auto then have "B{is compact in}((CoFinite X){restricted to}B)" using cofinite_compact union_cocardinal unfolding Cofinite_def by auto then have "B{is compact in}(CoFinite X)" using compact_subspace_imp_compact by auto ultimately have "∃c∈Pow(B). x∈Interior(c,CoFinite X)∧ c{is compact in}(CoFinite X)" by auto } then have "(∀x∈⋃(CoFinite X). ∀b∈(CoFinite X). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,CoFinite X) ∧ c{is compact in}(CoFinite X)))" by auto then show ?thesis unfolding IsLocallyComp_def IsLocally_def[OF cof1] by auto qed text{*In every locally compact space, by definition, every point has a compact neighbourhood.*} theorem (in topology0) locally_compact_exist_compact_neig: assumes "T{is locally-compact}" shows "∀x∈⋃T. ∃A∈Pow(⋃T). A{is compact in}T ∧ x∈int(A)" proof- { fix x assume "x∈⋃T" moreover then have "⋃T≠0" by auto have "⋃T∈T" using union_open topSpaceAssum by auto ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ c{is compact in}T" using assms IsLocally_def topSpaceAssum unfolding IsLocallyComp_def by auto then have "∃c∈Pow(⋃T). c{is compact in}T ∧ x∈int(c)" by auto } then show ?thesis by auto qed text{*In Hausdorff spaces, the previous result is an equivalence.*} theorem (in topology0) exist_compact_neig_T2_imp_locally_compact: assumes "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A) ∧ A{is compact in}T" "T{is T⇩_{2}}" shows "T{is locally-compact}" proof- { fix x assume "x∈⋃T" with assms(1) obtain A where "A∈Pow(⋃T)" "x∈int(A)" and Acom:"A{is compact in}T" by blast then have Acl:"A{is closed in}T" using in_t2_compact_is_cl assms(2) by auto then have sub:"A⊆⋃T" unfolding IsClosed_def by auto { fix U assume "U∈T" "x∈U" let ?V="int(A∩U)" from `x∈U` `x∈int(A)` have "x∈U∩(int (A))" by auto moreover from `U∈T` have "U∩(int(A))∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover have "U∩(int(A))⊆A∩U" using Top_2_L1 by auto ultimately have "x∈?V" using Top_2_L5 by blast have "?V⊆A" using Top_2_L1 by auto then have "cl(?V)⊆A" using Acl Top_3_L13 by auto then have "A∩cl(?V)=cl(?V)" by auto moreover have clcl:"cl(?V){is closed in}T" using cl_is_closed `?V⊆A` `A⊆⋃T` by auto ultimately have comp:"cl(?V){is compact in}T" using Acom compact_closed[of "A""nat""T""cl(?V)"] Compact_is_card_nat by auto { then have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat by auto moreover have "⋃(T{restricted to}cl(?V))=cl(?V)" unfolding RestrictedTo_def using clcl unfolding IsClosed_def by auto moreover ultimately have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto } then have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto moreover have "(T{restricted to}cl(?V)){is T⇩_{2}}" using assms(2) T2_here clcl unfolding IsClosed_def by auto ultimately have "(T{restricted to}cl(?V)){is T⇩_{4}}" using topology0.T2_compact_is_normal unfolding topology0_def using Top_1_L4 unfolding isT4_def using T2_is_T1 by auto then have clvreg:"(T{restricted to}cl(?V)){is regular}" using topology0.T4_is_T3 unfolding topology0_def isT3_def using Top_1_L4 by auto have "?V⊆cl(?V)" using cl_contains_set `?V⊆A` `A⊆⋃T` by auto then have "?V∈(T{restricted to}cl(?V))" unfolding RestrictedTo_def using Top_2_L2 by auto with `x∈?V` obtain W where Wop:"W∈(T{restricted to}cl(?V))" and clcont:"Closure(W,(T{restricted to}cl(?V)))⊆?V" and cinW:"x∈W" using topology0.regular_imp_exist_clos_neig unfolding topology0_def using Top_1_L4 clvreg by blast from clcont Wop have "W⊆?V" using topology0.cl_contains_set unfolding topology0_def using Top_1_L4 by auto with Wop have "W∈(T{restricted to}cl(?V)){restricted to}?V" unfolding RestrictedTo_def by auto moreover from `?V⊆A` `A⊆⋃T` have "?V⊆⋃T" by auto then have "?V⊆cl(?V)""cl(?V)⊆⋃T" using `?V⊆cl(?V)` Top_3_L11(1) by auto then have "(T{restricted to}cl(?V)){restricted to}?V=(T{restricted to}?V)" using subspace_of_subspace by auto ultimately have "W∈(T{restricted to}?V)" by auto then obtain UU where "UU∈T" "W=UU∩?V" unfolding RestrictedTo_def by auto then have "W∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover have "W⊆Closure(W,(T{restricted to}cl(?V)))" using topology0.cl_contains_set unfolding topology0_def using Top_1_L4 Wop by auto ultimately have A1:"x∈int(Closure(W,(T{restricted to}cl(?V))))" using Top_2_L6 cinW by auto from clcont have A2:"Closure(W,(T{restricted to}cl(?V)))⊆U" using Top_2_L1 by auto have clwcl:"Closure(W,(T{restricted to}cl(?V))) {is closed in}(T{restricted to}cl(?V))" using topology0.cl_is_closed Top_1_L4 Wop unfolding topology0_def by auto from comp have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat by auto with clwcl have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V)))))){is compact in}(T{restricted to}cl(?V))" using compact_closed Compact_is_card_nat by auto moreover from clcont have cont:"(Closure(W,(T{restricted to}cl(?V))))⊆cl(?V)" using cl_contains_set `?V⊆A``A⊆⋃T` by blast then have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V))))))=Closure(W,(T{restricted to}cl(?V)))" by auto ultimately have "Closure(W,(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto then have "Closure(W,(T{restricted to}cl(?V))){is compact in}T" using compact_subspace_imp_compact[of "Closure(W,T{restricted to}cl(?V))"] cont by auto with A1 A2 have "∃c∈Pow(U). x∈int(c)∧c{is compact in}T" by auto } then have "∀U∈T. x∈U ⟶ (∃c∈Pow(U). x∈int(c)∧c{is compact in}T)" by auto } then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] IsLocallyComp_def by auto qed subsection{*Compactification by one point*} text{*Given a topological space, we can always add one point to the space and get a new compact topology; as we will check in this section.*} definition OPCompactification ("{one-point compactification of}_" 90) where "{one-point compactification of}T≡T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}" text{*Firstly, we check that what we defined is indeed a topology.*} theorem (in topology0) op_comp_is_top: shows "({one-point compactification of}T){is a topology}" unfolding IsATopology_def proof(safe) fix M assume "M⊆{one-point compactification of}T" then have disj:"M⊆T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}" unfolding OPCompactification_def by auto let ?MT="{A∈M. A∈T}" have "?MT⊆T" by auto then have c1:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto let ?MK="{A∈M. A∉T}" have "⋃M=⋃?MK ∪ ⋃?MT" by auto from disj have "?MK⊆{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto moreover have N:"⋃T∉(⋃T)" using mem_not_refl by auto { fix B assume "B∈M" "B∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}" then obtain K where "K∈Pow(⋃T)" "B={⋃T}∪((⋃T)-K)" by auto with N have "⋃T∈B" by auto with N have "B∉T" by auto with `B∈M` have "B∈?MK" by auto } then have "{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}⊆?MK" by auto ultimately have MK_def:"?MK={A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto let ?KK="{K∈Pow(⋃T). {⋃T}∪((⋃T)-K)∈?MK}" { assume "?MK=0" then have "⋃M=⋃?MT" by auto then have "⋃M∈T" using c1 by auto then have "⋃M∈{one-point compactification of}T" unfolding OPCompactification_def by auto } moreover { assume "?MK≠0" then obtain A where "A∈?MK" by auto then obtain K1 where "A={⋃T}∪((⋃T)-K1)" "K1∈Pow(⋃T)" "K1{is closed in}T" "K1{is compact in}T" using MK_def by auto with `A∈?MK` have "⋂?KK⊆K1" by auto from `A∈?MK` `A={⋃T}∪((⋃T)-K1)` `K1∈Pow(⋃T)` have "?KK≠0" by blast { fix K assume "K∈?KK" then have "{⋃T}∪((⋃T)-K)∈?MK" "K⊆⋃T" by auto then obtain KK where A:"{⋃T}∪((⋃T)-K)={⋃T}∪((⋃T)-KK)" "KK⊆⋃T" "KK{is compact in}T" "KK{is closed in}T" using MK_def by auto note A(1) moreover have "(⋃T)-K⊆{⋃T}∪((⋃T)-K)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-KK)" by auto ultimately have "(⋃T)-K⊆{⋃T}∪((⋃T)-KK)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-K)" by auto moreover from N have "⋃T∉(⋃T)-K" "⋃T∉(⋃T)-KK" by auto ultimately have "(⋃T)-K⊆((⋃T)-KK)" "(⋃T)-KK⊆((⋃T)-K)" by auto then have "(⋃T)-K=(⋃T)-KK" by auto moreover from `K⊆⋃T` have "K=(⋃T)-((⋃T)-K)" by auto ultimately have "K=(⋃T)-((⋃T)-KK)" by auto with `KK⊆⋃T` have "K=KK" by auto with A(4) have "K{is closed in}T" by auto } then have "∀K∈?KK. K{is closed in}T" by auto with `?KK≠0` have "(⋂?KK){is closed in}T" using Top_3_L4 by auto with `K1{is compact in}T` have "(K1∩(⋂?KK)){is compact in}T" using Compact_is_card_nat compact_closed[of "K1""nat""T""⋂?KK"] by auto moreover from `⋂?KK⊆K1` have "K1∩(⋂?KK)=(⋂?KK)" by auto ultimately have "(⋂?KK){is compact in}T" by auto with `(⋂?KK){is closed in}T` `⋂?KK⊆K1` `K1∈Pow(⋃T)` have "({⋃T}∪((⋃T)-(⋂?KK)))∈({one-point compactification of}T)" unfolding OPCompactification_def by blast have t:"⋃?MK=⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" using MK_def by auto { fix x assume "x∈⋃?MK" with t have "x∈⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto then have "∃AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}. x∈AA" using Union_iff by auto then obtain AA where AAp:"AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" "x∈AA" by auto then obtain K2 where "AA={⋃T}∪((⋃T)-K2)" "K2∈Pow(⋃T)""K2{is compact in}T" "K2{is closed in}T" by auto with `x∈AA` have "x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)" by auto from `K2∈Pow(⋃T)` `AA={⋃T}∪((⋃T)-K2)` AAp(1) MK_def have "K2∈?KK" by auto then have "⋂?KK⊆K2" by auto with `x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)` have "x=⋃T∨(x∈⋃T ∧ x∉⋂?KK)" by auto then have "x∈{⋃T}∪((⋃T)-(⋂?KK))" by auto } then have "⋃?MK⊆{⋃T}∪((⋃T)-(⋂?KK))" by auto moreover { fix x assume "x∈{⋃T}∪((⋃T)-(⋂?KK))" then have "x=⋃T∨(x∈(⋃T)∧ x∉⋂?KK)" by auto with `?KK≠0` obtain K2 where "K2∈?KK" "x=⋃T∨(x∈⋃T∧ x∉K2)" by auto then have "{⋃T}∪((⋃T)-K2)∈?MK" by auto with `x=⋃T∨(x∈⋃T∧ x∉K2)` have "x∈⋃?MK" by auto } then have "{⋃T}∪((⋃T)-(⋂?KK))⊆⋃?MK" by (safe,auto) ultimately have "⋃?MK={⋃T}∪((⋃T)-(⋂?KK))" by blast from `⋃?MT∈T` have "⋃T-(⋃T-⋃?MT)=⋃?MT" by auto with `⋃?MT∈T` have "(⋃T-⋃?MT){is closed in}T" unfolding IsClosed_def by auto have "((⋃T)-(⋂?KK))∪(⋃T-(⋃T-⋃?MT))=(⋃T)-((⋂?KK)∩(⋃T-⋃?MT))" by auto then have "({⋃T}∪((⋃T)-(⋂?KK)))∪(⋃T-(⋃T-⋃?MT))={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto with `⋃?MK={⋃T}∪((⋃T)-(⋂?KK))``⋃T-(⋃T-⋃?MT)=⋃?MT` have "⋃?MK∪⋃?MT={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto with `⋃M=⋃?MK ∪⋃?MT` have unM:"⋃M={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto have "((⋂?KK)∩(⋃T-⋃?MT)) {is closed in}T" using `(⋂?KK){is closed in}T``(⋃T-(⋃?MT)){is closed in}T` Top_3_L5 by auto moreover note `(⋃T-(⋃?MT)){is closed in}T` `(⋂?KK){is compact in}T` then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact of cardinal}nat{in}T" using compact_closed[of "⋂?KK""nat""T""(⋃T-⋃?MT)"] Compact_is_card_nat by auto then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact in}T" using Compact_is_card_nat by auto ultimately have "{⋃T}∪(⋃T-((⋂?KK)∩(⋃T-⋃?MT)))∈{one-point compactification of}T" unfolding OPCompactification_def IsClosed_def by auto with unM have "⋃M∈{one-point compactification of}T" by auto } ultimately show "⋃M∈{one-point compactification of}T" by auto next fix U V assume "U∈{one-point compactification of}T" and "V∈{one-point compactification of}T" then have A:"U∈T∨(∃KU∈Pow(⋃T). U={⋃T}∪(⋃T-KU)∧KU{is closed in}T∧KU{is compact in}T)" "V∈T∨(∃KV∈Pow(⋃T). V={⋃T}∪(⋃T-KV)∧KV{is closed in}T∧KV{is compact in}T)" unfolding OPCompactification_def by auto have N:"⋃T∉(⋃T)" using mem_not_refl by auto { assume "U∈T""V∈T" then have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto } moreover { assume "U∈T""V∉T" then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)" using A(2) by auto with N `U∈T` have "⋃T∉U" by auto then have "⋃T∉U∩V" by auto then have "U∩V=U∩(⋃T-KV)" using V(3) by auto moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto with `U∈T` have "U∩(⋃T-KV)∈T" using topSpaceAssum unfolding IsATopology_def by auto with `U∩V=U∩(⋃T-KV)` have "U∩V∈T" by auto then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto } moreover { assume "U∉T""V∈T" then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""U={⋃T}∪(⋃T-KV)" using A(1) by auto with N `V∈T` have "⋃T∉V" by auto then have "⋃T∉U∩V" by auto then have "U∩V=(⋃T-KV)∩V" using V(3) by auto moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto with `V∈T` have "(⋃T-KV)∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto with `U∩V=(⋃T-KV)∩V` have "U∩V∈T" by auto then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto } moreover { assume "U∉T""V∉T" then obtain KV KU where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)" and U:"KU{is closed in}T""KU{is compact in}T""U={⋃T}∪(⋃T-KU)" using A by auto with V(3) U(3) have "⋃T∈U∩V" by auto then have "U∩V={⋃T}∪((⋃T-KV)∩(⋃T-KU))" using V(3) U(3) by auto moreover have "⋃T-KV∈T""⋃T-KU∈T" using V(1) U(1) unfolding IsClosed_def by auto then have "(⋃T-KV)∩(⋃T-KU)∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "(⋃T-KV)∩(⋃T-KU)=⋃T-(⋃T-((⋃T-KV)∩(⋃T-KU)))" by auto moreover with `(⋃T-KV)∩(⋃T-KU)∈T` have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is closed in}T" unfolding IsClosed_def by auto moreover from V(1) U(1) have "(⋃T-(⋃T-KV)∩(⋃T-KU))=KV∪KU" unfolding IsClosed_def by auto with V(2) U(2) have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is compact in}T" using union_compact[of "KV""nat""T""KU"] Compact_is_card_nat InfCard_nat by auto ultimately have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto } ultimately show "U∩V∈{one-point compactification of}T" by auto qed text{*The original topology is an open subspace of the new topology.*} theorem (in topology0) open_subspace: shows "⋃T∈{one-point compactification of}T" and "({one-point compactification of}T){restricted to}⋃T=T" proof- show "⋃T∈{one-point compactification of}T" unfolding OPCompactification_def using topSpaceAssum unfolding IsATopology_def by auto have "T⊆({one-point compactification of}T){restricted to}⋃T" unfolding OPCompactification_def RestrictedTo_def by auto moreover { fix A assume "A∈({one-point compactification of}T){restricted to}⋃T" then obtain R where "R∈({one-point compactification of}T)" "A=⋃T∩R" unfolding RestrictedTo_def by auto then obtain K where K:"R∈T ∨ (R={⋃T}∪(⋃T-K) ∧ K{is closed in}T)" unfolding OPCompactification_def by auto with `A=⋃T∩R` have "(A=R∧R∈T)∨(A=⋃T-K ∧ K{is closed in}T)" using mem_not_refl unfolding IsClosed_def by auto with K have "A∈T" unfolding IsClosed_def by auto } ultimately show "({one-point compactification of}T){restricted to}⋃T=T" by auto qed text{*We added only one new point to the space.*} lemma (in topology0) op_compact_total: shows "⋃({one-point compactification of}T)={⋃T}∪(⋃T)" proof- have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto moreover note Top_3_L2 ultimately have TT:"0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto have "⋃({one-point compactification of}T)=(⋃T)∪(⋃{{⋃T}∪(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" unfolding OPCompactification_def by blast also have "…=(⋃T)∪{⋃T}∪(⋃{(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" using TT by auto ultimately show "⋃({one-point compactification of}T)={⋃T}∪(⋃T)" by auto qed text{*The one point compactification, gives indeed a compact topological space.*} theorem (in topology0) compact_op: shows "({⋃T}∪(⋃T)){is compact in}({one-point compactification of}T)" unfolding IsCompact_def proof(safe) have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto moreover note Top_3_L2 ultimately have "0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto then have "{⋃T}∪(⋃T)∈{one-point compactification of}T" unfolding OPCompactification_def by auto then show "⋃T ∈ ⋃{one-point compactification of}T" by auto next fix x B assume "x∈B""B∈T" then show "x∈⋃({one-point compactification of}T)" using open_subspace by auto next fix M assume A:"M⊆({one-point compactification of}T)" "{⋃T} ∪ ⋃T ⊆ ⋃M" then obtain R where "R∈M""⋃T∈R" by auto have "⋃T∉⋃T" using mem_not_refl by auto with `R∈M` `⋃T∈R` A(1) obtain K where K:"R={⋃T}∪(⋃T-K)" "K{is compact in}T""K{is closed in}T" unfolding OPCompactification_def by auto from K(1,2) have B:"{⋃T} ∪ (⋃T) = R ∪ K" unfolding IsCompact_def by auto with A(2) have "K⊆⋃M" by auto from K(2) have "K{is compact in}(({one-point compactification of}T){restricted to}⋃T)" using open_subspace(2) by auto then have "K{is compact in}({one-point compactification of}T)" using compact_subspace_imp_compact `K{is closed in}T` unfolding IsClosed_def by auto with `K⊆⋃M` A(1) have "(∃N∈FinPow(M). K ⊆ ⋃N)" unfolding IsCompact_def by auto then obtain N where "N∈FinPow(M)" "K⊆⋃N" by auto with `R∈M` have "(N ∪{R})∈FinPow(M)""R∪K⊆⋃(N∪{R})" unfolding FinPow_def by auto with B show "∃N∈FinPow(M). {⋃T} ∪ (⋃T)⊆⋃N" by auto qed text{*The one point compactification is Hausdorff iff the original space is also Hausdorff and locally compact.*} lemma (in topology0) op_compact_T2_1: assumes "({one-point compactification of}T){is T⇩_{2}}" shows "T{is T⇩_{2}}" using T2_here[OF assms, of "⋃T"] open_subspace by auto lemma (in topology0) op_compact_T2_2: assumes "({one-point compactification of}T){is T⇩_{2}}" shows "T{is locally-compact}" proof- { fix x assume "x∈⋃T" then have "x∈{⋃T}∪(⋃T)" by auto moreover have "⋃T∈{⋃T}∪(⋃T)" by auto moreover from `x∈⋃T` have "x≠⋃T" using mem_not_refl by auto ultimately have "∃U∈{one-point compactification of}T. ∃V∈{one-point compactification of}T. x ∈ U ∧ (⋃T) ∈ V ∧ U ∩ V = 0" using assms op_compact_total unfolding isT2_def by auto then obtain U V where UV:"U∈{one-point compactification of}T""V∈{one-point compactification of}T" "x∈U""⋃T∈V""U∩V=0" by auto from `V∈{one-point compactification of}T` `⋃T∈V` mem_not_refl obtain K where K:"V={⋃T}∪(⋃T-K)""K{is closed in}T""K{is compact in}T" unfolding OPCompactification_def by auto from `U∈{one-point compactification of}T` have "U⊆{⋃T}∪(⋃T)" unfolding OPCompactification_def using op_compact_total by auto with `U∩V=0` K have "U⊆K""K⊆⋃T" unfolding IsClosed_def by auto then have "(⋃T)∩U=U" by auto moreover from UV(1) have "((⋃T)∩U)∈({one-point compactification of}T){restricted to}⋃T" unfolding RestrictedTo_def by auto ultimately have "U∈T" using open_subspace(2) by auto with `x∈U``U⊆K` have "x∈int(K)" using Top_2_L6 by auto with `K⊆⋃T` `K{is compact in}T` have "∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto } then have "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto then show ?thesis using op_compact_T2_1[OF assms] exist_compact_neig_T2_imp_locally_compact by auto qed lemma (in topology0) op_compact_T2_3: assumes "T{is locally-compact}" "T{is T⇩_{2}}" shows "({one-point compactification of}T){is T⇩_{2}}" proof- { fix x y assume "x≠y""x∈⋃({one-point compactification of}T)""y∈⋃({one-point compactification of}T)" then have S:"x∈{⋃T}∪(⋃T)""y∈{⋃T}∪(⋃T)" using op_compact_total by auto { assume "x∈⋃T""y∈⋃T" with `x≠y` have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(2) unfolding isT2_def by auto then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" unfolding OPCompactification_def by auto } moreover { assume "x∉⋃T∨y∉⋃T" with S have "x=⋃T∨y=⋃T" by auto with `x≠y` have "(x=⋃T∧y≠⋃T)∨(y=⋃T∧x≠⋃T)" by auto with S have "(x=⋃T∧y∈⋃T)∨(y=⋃T∧x∈⋃T)" by auto then obtain Ky Kx where "(x=⋃T∧ Ky{is compact in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧x∈int(Kx))" using assms(1) locally_compact_exist_compact_neig by blast then have "(x=⋃T∧ Ky{is compact in}T∧ Ky{is closed in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧ Kx{is closed in}T∧x∈int(Kx))" using in_t2_compact_is_cl assms(2) by auto then have "(x∈{⋃T}∪(⋃T-Ky)∧y∈int(Ky)∧ Ky{is compact in}T∧ Ky{is closed in}T)∨(y∈{⋃T}∪(⋃T-Kx)∧x∈int(Kx)∧ Kx{is compact in}T∧ Kx{is closed in}T)" by auto moreover { fix K assume A:"K{is closed in}T""K{is compact in}T" then have "K⊆⋃T" unfolding IsClosed_def by auto moreover have "⋃T∉⋃T" using mem_not_refl by auto ultimately have "({⋃T}∪(⋃T-K))∩K=0" by auto then have "({⋃T}∪(⋃T-K))∩int(K)=0" using Top_2_L1 by auto moreover from A have "{⋃T}∪(⋃T-K)∈({one-point compactification of}T)" unfolding OPCompactification_def IsClosed_def by auto moreover have "int(K)∈({one-point compactification of}T)" using Top_2_L2 unfolding OPCompactification_def by auto ultimately have "int(K)∈({one-point compactification of}T)∧{⋃T}∪(⋃T-K)∈({one-point compactification of}T)∧({⋃T}∪(⋃T-K))∩int(K)=0" by auto } ultimately have "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0) ∨ ({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)" by auto moreover { assume "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0)" then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "int(Ky)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0" "{⋃T}∪(⋃T-Ky)"] by auto } moreover { assume "({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)" then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "{⋃T}∪(⋃T-Kx)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0""int(Kx)" ] by blast } ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto } ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto } then show ?thesis unfolding isT2_def by auto qed text{*In conclusion, every locally compact Hausdorff topological space is regular; since this property is hereditary.*} corollary (in topology0) locally_compact_T2_imp_regular: assumes "T{is locally-compact}" "T{is T⇩_{2}}" shows "T{is regular}" proof- from assms have "( {one-point compactification of}T) {is T⇩_{2}}" using op_compact_T2_3 by auto then have "({one-point compactification of}T) {is T⇩_{4}}" unfolding isT4_def using T2_is_T1 topology0.T2_compact_is_normal op_comp_is_top unfolding topology0_def using op_compact_total compact_op by auto then have "({one-point compactification of}T) {is T⇩_{3}}" using topology0.T4_is_T3 op_comp_is_top unfolding topology0_def by auto then have "({one-point compactification of}T) {is regular}" using isT3_def by auto moreover have "⋃T⊆⋃({one-point compactification of}T)" using op_compact_total by auto ultimately have "(({one-point compactification of}T){restricted to}⋃T) {is regular}" using regular_here by auto then show "T{is regular}" using open_subspace(2) by auto qed text{*This last corollary has an explanation: In Hausdorff spaces, compact sets are closed and regular spaces are exactly the "locally closed spaces"(those which have a neighbourhood basis of closed sets). So the neighbourhood basis of compact sets also works as the neighbourhood basis of closed sets we needed to find.*} definition IsLocallyClosed ("_{is locally-closed}") where "T{is locally-closed} ≡ T{is locally}(λB TT. B{is closed in}TT)" lemma (in topology0) regular_locally_closed: shows "T{is regular} ⟷ (T{is locally-closed})" proof assume "T{is regular}" then have a:"∀x∈⋃T. ∀U∈T. (x∈U) ⟶ (∃V∈T. x ∈ V ∧ cl(V) ⊆ U)" using regular_imp_exist_clos_neig by auto { fix x b assume "x∈⋃T""b∈T""x∈b" with a obtain V where "V∈T""x∈V""cl(V)⊆b" by blast note `cl(V)⊆b` moreover from `V∈T` have "V⊆⋃T" by auto then have "V⊆cl(V)" using cl_contains_set by auto with `x∈V``V∈T` have "x∈int(cl(V))" using Top_2_L6 by auto moreover from `V⊆⋃T` have "cl(V){is closed in}T" using cl_is_closed by auto ultimately have "x∈int(cl(V))""cl(V)⊆b""cl(V){is closed in}T" by auto then have "∃K∈Pow(b). x∈int(K)∧K{is closed in}T" by auto } then show "T{is locally-closed}" unfolding IsLocally_def[OF topSpaceAssum] IsLocallyClosed_def by auto next assume "T{is locally-closed}" then have a:"∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃K∈Pow(b). x∈int(K)∧K{is closed in}T)" unfolding IsLocally_def[OF topSpaceAssum] IsLocallyClosed_def by auto { fix x b assume "x∈⋃T""b∈T""x∈b" with a obtain K where K:"K⊆b""x∈int(K)""K{is closed in}T" by blast have "int(K)⊆K" using Top_2_L1 by auto with K(3) have "cl(int(K))⊆K" using Top_3_L13 by auto with K(1) have "cl(int(K))⊆b" by auto moreover have "int(K)∈T" using Top_2_L2 by auto moreover note `x∈int(K)` ultimately have "∃V∈T. x∈V∧ cl(V)⊆b" by auto } then have "∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃V∈T. x∈V∧ cl(V)⊆b)" by auto then show "T{is regular}" using exist_clos_neig_imp_regular by auto qed subsection{*Hereditary properties and local properties*} text{*In this section, we prove a relation between a property and its local property for hereditary properties. Then we apply it to locally-Hausdorff or locally-$T_2$. We also prove the relation between locally-$T_2$ and another property that appeared when considering anti-properties, the anti-hyperconnectness.*} text{*If a property is hereditary in open sets, then local properties are equivalent to find just one open neighbourhood with that property instead of a whole local basis.*} lemma (in topology0) her_P_is_loc_P: assumes "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧P(B,TT) ⟶ P(B∩A,TT)" shows "(T{is locally}P) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧P(A,T))" proof assume A:"T{is locally}P" { fix x assume x:"x∈⋃T" with A have "∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈int(c)∧P(c,T))" unfolding IsLocally_def[OF topSpaceAssum] by auto moreover note x moreover have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ P(c,T)" by auto then obtain c where c:"c⊆⋃T""x∈int(c)""P(c,T)" by auto have P:"int(c)∈T" using Top_2_L2 by auto moreover from c(1,3) topSpaceAssum assms have "∀A∈T. P(c∩A,T)" by auto ultimately have "P(c∩int(c),T)" by auto moreover from Top_2_L1[of "c"] have "int(c)⊆c" by auto then have "c∩int(c)=int(c)" by auto ultimately have "P(int(c),T)" by auto with P c(2) have "∃V∈T. x∈V∧P(V,T)" by auto } then show "∀x∈⋃T. ∃V∈T. x∈V∧P(V,T)" by auto next assume A:"∀x∈⋃T. ∃A∈T. x ∈ A ∧ P(A, T)" { fix x assume x:"x∈⋃T" { fix b assume b:"x∈b""b∈T" from x A obtain A where A_def:"A∈T""x∈A""P(A,T)" by auto from A_def(1,3) assms topSpaceAssum have "∀G∈T. P(A∩G,T)" by auto with b(2) have "P(A∩b,T)" by auto moreover from b(1) A_def(2) have "x∈A∩b" by auto moreover have "A∩b∈T" using b(2) A_def(1) topSpaceAssum IsATopology_def by auto then have "int(A∩b)=A∩b" using Top_2_L3 by auto ultimately have "x∈int(A∩b)∧P(A∩b,T)" by auto then have "∃c∈Pow(b). x∈int(c)∧P(c,T)" by auto } then have "∀b∈T. x∈b⟶(∃c∈Pow(b). x∈int(c)∧P(c,T))" by auto } then show "T{is locally}P" unfolding IsLocally_def[OF topSpaceAssum] by auto qed definition IsLocallyT2 ("_{is locally-T⇩_{2}}" 70) where "T{is locally-T⇩_{2}}≡T{is locally}(λB. λT. (T{restricted to}B){is T⇩_{2}})" text{*Since $T_2$ is an hereditary property, we can apply the previous lemma.*} corollary (in topology0) loc_T2: shows "(T{is locally-T⇩_{2}}) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧(T{restricted to}A){is T⇩_{2}})" proof- { fix TT B A assume TT:"TT{is a topology}" "(TT{restricted to}B){is T⇩_{2}}" "A∈TT""B∈Pow(⋃TT)" then have s:"B∩A⊆B""B⊆⋃TT" by auto then have "(TT{restricted to}(B∩A))=(TT{restricted to}B){restricted to}(B∩A)" using subspace_of_subspace by auto moreover have "⋃(TT{restricted to}B)=B" unfolding RestrictedTo_def using s(2) by auto then have "B∩A⊆⋃(TT{restricted to}B)" using s(1) by auto moreover note TT(2) ultimately have "(TT{restricted to}(B∩A)){is T⇩_{2}}" using T2_here by auto } then have "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧(TT{restricted to}B){is T⇩_{2}} ⟶ (TT{restricted to}(B∩A)){is T⇩_{2}}" by auto with her_P_is_loc_P[where P="λA. λTT. (TT{restricted to}A){is T⇩_{2}}"] show ?thesis unfolding IsLocallyT2_def by auto qed text{*First, we prove that a locally-$T_2$ space is anti-hyperconnected.*} text{*Before starting, let's prove that an open subspace of an hyperconnected space is hyperconnected.*} lemma(in topology0) open_subspace_hyperconn: assumes "T{is hyperconnected}" "U∈T" shows "(T{restricted to}U){is hyperconnected}" proof- { fix A B assume "A∈(T{restricted to}U)""B∈(T{restricted to}U)""A∩B=0" then obtain AU BU where "A=U∩AU""B=U∩BU" "AU∈T""BU∈T" unfolding RestrictedTo_def by auto then have "A∈T""B∈T" using topSpaceAssum assms(2) unfolding IsATopology_def by auto with `A∩B=0` have "A=0∨B=0" using assms(1) unfolding IsHConnected_def by auto } then show ?thesis unfolding IsHConnected_def by auto qed lemma(in topology0) locally_T2_is_antiHConn: assumes "T{is locally-T⇩_{2}}" shows "T{is anti-}IsHConnected" proof- { fix A assume A:"A∈Pow(⋃T)""(T{restricted to}A){is hyperconnected}" { fix x assume "x∈A" with A(1) have "x∈⋃T" by auto moreover have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have "∃c∈Pow(⋃T). x ∈ int(c) ∧ (T {restricted to} c) {is T⇩_{2}}" using assms unfolding IsLocallyT2_def IsLocally_def[OF topSpaceAssum] by auto then obtain c where c:"c∈Pow(⋃T)""x∈int(c)""(T {restricted to} c) {is T⇩_{2}}" by auto have "⋃(T {restricted to} c)=(⋃T)∩c" unfolding RestrictedTo_def by auto with `c∈Pow(⋃T)``⋃T∈T` have tot:"⋃(T {restricted to} c)=c" by auto have "int(c)∈T" using Top_2_L2 by auto then have "A∩(int(c))∈(T{restricted to}A)" unfolding RestrictedTo_def by auto with A(2) have "((T{restricted to}A){restricted to}(A∩(int(c)))){is hyperconnected}" using topology0.open_subspace_hyperconn unfolding topology0_def using Top_1_L4 by auto then have "(T{restricted to}(A∩(int(c)))){is hyperconnected}" using subspace_of_subspace[of "A∩(int(c))" "A""T"] A(1) by force moreover have "int(c)⊆c" using Top_2_L1 by auto then have sub:"A∩(int(c))⊆c" by auto then have "A∩(int(c))⊆⋃(T {restricted to} c)" using tot by auto then have "((T {restricted to} c){restricted to}(A∩(int(c)))) {is T⇩_{2}}" using T2_here[OF c(3)] by auto with sub have "(T {restricted to}(A∩(int(c)))){is T⇩_{2}}" using subspace_of_subspace[of "A∩(int(c))" "c""T"] `c∈Pow(⋃T)` by auto ultimately have "(T{restricted to}(A∩(int(c)))){is hyperconnected}""(T {restricted to}(A∩(int(c)))){is T⇩_{2}}" by auto then have "(T{restricted to}(A∩(int(c)))){is hyperconnected}""(T {restricted to}(A∩(int(c)))){is anti-}IsHConnected" using topology0.T2_imp_anti_HConn unfolding topology0_def using Top_1_L4 by auto moreover have "⋃(T{restricted to}(A∩(int(c))))=(⋃T)∩A∩(int(c))" unfolding RestrictedTo_def by auto with A(1) Top_2_L2 have "⋃(T{restricted to}(A∩(int(c))))=A∩(int(c))" by auto then have "A∩(int(c))⊆⋃(T{restricted to}(A∩(int(c))))" by auto moreover have "A∩(int(c))⊆⋃T" using A(1) Top_2_L2 by auto then have "(T{restricted to}(A∩(int(c)))){restricted to}(A∩(int(c)))=(T{restricted to}(A∩(int(c))))" using subspace_of_subspace[of "A∩(int(c))""A∩(int(c))""T"] by auto ultimately have "(A∩(int(c))){is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto then have "A∩(int(c))≲1" using HConn_spectrum by auto then have "(A∩(int(c))={x})" using lepoll_1_is_sing `x∈A``x∈int(c)` by auto then have "{x}∈(T{restricted to}A)" using `(A∩(int(c))∈(T{restricted to}A))` by auto } then have pointOpen:"∀x∈A. {x}∈(T{restricted to}A)" by auto { fix x y assume "x≠y""x∈A""y∈A" with pointOpen have "{x}∈(T{restricted to}A)""{y}∈(T{restricted to}A)""{x}∩{y}=0" by auto with A(2) have "{x}=0∨{y}=0" unfolding IsHConnected_def by auto then have "False" by auto } then have uni:"∀x∈A. ∀y∈A. x=y" by auto { assume "A≠0" then obtain x where "x∈A" by auto with uni have "A={x}" 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 have "A≲1" by auto then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto } then show ?thesis unfolding antiProperty_def by auto qed text{*Now we find a counter-example for: Every anti-hyperconnected space is locally-Hausdorff.*} text{*The example we are going to consider is the following. Put in $X$ an anti-hyperconnected topology, where an infinite number of points don't have finite sets as neighbourhoods. Then add a new point to the set, $p\notin X$. Consider the open sets on $X\cup {p}$ as the anti-hyperconnected topology and the open sets that contain $p$ are $p\cup A$ where $X\setminus A$ is finite.*} text{*This construction equals the one-point compactification iff $X$ is anti-compact; i.e., the only compact sets are the finite ones. In general this topology is contained in the one-point compactification topology, making it compact too.*} text{*It is easy to check that any open set containing $p$ meets infinite other non-empty open set. The question is if such a topology exists.*} theorem (in topology0) COF_comp_is_top: assumes "T{is T⇩_{1}}""¬(⋃T≺nat)" shows "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T) {is a topology}" proof- have N:"⋃T∉(⋃T)" using mem_not_refl by auto { fix M assume M:"M⊆((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)" let ?MT="{A∈M. A∈T}" let ?MK="{A∈M. A∉T}" have MM:"(⋃?MT)∪(⋃?MK)=⋃M" by auto have MN:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto then have sub:"?MK⊆({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" using M by auto then have "?MK⊆({one-point compactification of}(CoFinite (⋃T)))" by auto then have CO:"⋃?MK∈({one-point compactification of}(CoFinite (⋃T)))" using topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]] unfolding Cofinite_def IsATopology_def by auto { assume AS:"⋃?MK={⋃T}" moreover have "∀R∈?MK. R⊆⋃?MK" by auto ultimately have "∀R∈?MK. R⊆{⋃T}" by auto then have "∀R∈?MK. R={⋃T}∨R=0" by force moreover with sub have "∀R∈?MK. R=0" by auto then have "⋃?MK=0" by auto with AS have "False" by auto } with CO have CO2:"⋃?MK∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto { assume "⋃?MK∈(CoFinite (⋃T))" then have "⋃?MK∈T" using assms(1) T1_cocardinal_coarser by auto with MN have "{⋃?MT,⋃?MK}⊆(T)" by auto then have "(⋃?MT)∪(⋃?MK)∈T" using union_open[OF topSpaceAssum, of "{⋃?MT,⋃?MK}"] by auto then have "⋃M∈T" using MM by auto } moreover { assume "⋃?MK∉(CoFinite (⋃T))" with CO obtain B where "B{is compact in}(CoFinite (⋃T))""B{is closed in}(CoFinite (⋃T))" "⋃?MK={⋃CoFinite ⋃T}∪(⋃(CoFinite ⋃T)-B)" unfolding OPCompactification_def by auto then have MK:"⋃?MK={⋃T}∪(⋃T-B)""B{is closed in}(CoFinite (⋃T))" using union_cocardinal unfolding Cofinite_def by auto then have B:"B⊆⋃T" "B≺nat∨B=⋃T" using closed_sets_cocardinal unfolding Cofinite_def by auto { assume "B=⋃T" with MK have "⋃?MK={⋃T}" by auto then have "False" using CO2 by auto } with B have "B⊆⋃T" and natB:"B≺nat" by auto have "(⋃T-(⋃?MT))∩B⊆B" by auto then have "(⋃T-(⋃?MT))∩B≲B" using subset_imp_lepoll by auto then have "(⋃T-(⋃?MT))∩B≺nat" using natB lesspoll_trans1 by auto then have "((⋃T-(⋃?MT))∩B){is closed in}(CoFinite (⋃T))" using closed_sets_cocardinal B(1) unfolding Cofinite_def by auto then have "⋃T-((⋃T-(⋃?MT))∩B)∈(CoFinite (⋃T))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto also have "⋃T-((⋃T-(⋃?MT))∩B)=(⋃T-(⋃T-(⋃?MT)))∪(⋃T-B)" by auto also have "…=(⋃?MT)∪(⋃T-B)" by auto ultimately have P:"(⋃?MT)∪(⋃T-B)∈(CoFinite (⋃T))" by auto then have eq:"⋃T-(⋃T-((⋃?MT)∪(⋃T-B)))=(⋃?MT)∪(⋃T-B)" by auto from P eq have "(⋃T-((⋃?MT)∪(⋃T-B))){is closed in}(CoFinite (⋃T))" unfolding IsClosed_def using union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto moreover have "(⋃T-((⋃?MT)∪(⋃T-B)))∩⋃T=(⋃T-((⋃?MT)∪(⋃T-B)))" by auto then have "(CoFinite ⋃T){restricted to}(⋃T-((⋃?MT)∪(⋃T-B)))=CoFinite (⋃T-((⋃?MT)∪(⋃T-B)))" using subspace_cocardinal unfolding Cofinite_def by auto then have "(⋃T-((⋃?MT)∪(⋃T-B))){is compact in}((CoFinite ⋃T){restricted to}(⋃T-((⋃?MT)∪(⋃T-B))))" using cofinite_compact union_cocardinal unfolding Cofinite_def by auto then have "(⋃T-((⋃?MT)∪(⋃T-B))){is compact in}(CoFinite ⋃T)" using compact_subspace_imp_compact by auto ultimately have "{⋃T}∪(⋃T-(⋃T-((⋃?MT)∪(⋃T-B))))∈({one-point compactification of}(CoFinite (⋃T)))" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto with eq have "{⋃T}∪((⋃?MT)∪(⋃T-B))∈({one-point compactification of}(CoFinite (⋃T)))" by auto moreover have AA:"{⋃T}∪((⋃?MT)∪(⋃T-B))=((⋃?MT)∪(⋃?MK))" using MK(1) by auto ultimately have AA2:"((⋃?MT)∪(⋃?MK))∈({one-point compactification of}(CoFinite (⋃T)))" by auto { assume AS:"(⋃?MT)∪(⋃?MK)={⋃T}" from MN have T:"⋃T∉⋃?MT" using N by auto { fix x assume G:"x∈⋃?MT" then have "x∈(⋃?MT)∪(⋃?MK)" by auto with AS have "x∈{⋃T}" by auto then have "x=⋃T" by auto with T have "False" using G by auto } then have "⋃?MT=0" by auto with AS have "(⋃?MK)={⋃T}" by auto then have "False" using CO2 by auto } with AA2 have "((⋃?MT)∪(⋃?MK))∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto with MM have "⋃M∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto } ultimately have "⋃M∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } then have "∀M∈Pow((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T). ⋃M∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto moreover { fix U V assume "U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T""V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" moreover { assume "U∈T""V∈T" then have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } moreover { assume UV:"U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})""V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})" then have O:"U∩V∈({one-point compactification of}(CoFinite (⋃T)))" using topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]] unfolding Cofinite_def IsATopology_def by auto then have "⋃T∩(U∩V)∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T" unfolding RestrictedTo_def by auto then have "⋃T∩(U∩V)∈CoFinite ⋃T" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]] union_cocardinal unfolding Cofinite_def by auto from UV have "U≠{⋃T}""V≠{⋃T}""⋃T∩U∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T""⋃T∩V∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T" unfolding RestrictedTo_def by auto then have R:"U≠{⋃T}""V≠{⋃T}""⋃T∩U∈CoFinite ⋃T""⋃T∩V∈CoFinite ⋃T" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]] union_cocardinal unfolding Cofinite_def by auto from UV have "U⊆⋃({one-point compactification of}(CoFinite (⋃T)))""V⊆⋃({one-point compactification of}(CoFinite (⋃T)))" by auto then have "U⊆{⋃T}∪⋃T""V⊆{⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat]] union_cocardinal unfolding Cofinite_def by auto then have E:"U=(⋃T∩U)∪({⋃T}∩U)""V=(⋃T∩V)∪({⋃T}∩V)""U∩V=(⋃T∩U∩V)∪({⋃T}∩U∩V)" by auto { assume Q:"U∩V={⋃T}" then have RR:"⋃T∩(U∩V)=0" using N by auto { assume "⋃T∩U=0" with E(1) have "U={⋃T}∩U" by auto also have "…⊆{⋃T}" by auto ultimately have "U⊆{⋃T}" by auto then have "U=0∨U={⋃T}" by auto with R(1) have "U=0" by auto then have "U∩V=0" by auto then have "False" using Q by auto } moreover { assume "⋃T∩V=0" with E(2) have "V={⋃T}∩V" by auto also have "…⊆{⋃T}" by auto ultimately have "V⊆{⋃T}" by auto then have "V=0∨V={⋃T}" by auto with R(2) have "V=0" by auto then have "U∩V=0" by auto then have "False" using Q by auto } moreover { assume "⋃T∩U≠0""⋃T∩V≠0" with R(3,4) have "(⋃T∩U)∩(⋃T∩V)≠0" using Cofinite_nat_HConn[OF assms(2)] unfolding IsHConnected_def by auto then have "⋃T∩(U∩V)≠0" by auto then have "False" using RR by auto } ultimately have "False" by auto } with O have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } moreover { assume UV:"U∈T""V∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" from UV(2) obtain B where "V∈(CoFinite ⋃T)∨(V={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto with assms(1) have "V∈T∨(V={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using T1_cocardinal_coarser by auto then have "V∈T∨(U∩V=U∩(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using UV(1) N by auto then have "V∈T∨(U∩V=U∩(⋃T-B)∧(⋃T-B)∈(CoFinite (⋃T)))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto then have "V∈T∨(U∩V=U∩(⋃T-B)∧(⋃T-B)∈T)" using assms(1) T1_cocardinal_coarser by auto with UV(1) have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } moreover { assume UV:"U∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}""V∈T" from UV(1) obtain B where "U∈(CoFinite ⋃T)∨(U={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto with assms(1) have "U∈T∨(U={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using T1_cocardinal_coarser by auto then have "U∈T∨(U∩V=(⋃T-B)∩V∧B{is closed in}(CoFinite (⋃T)))" using UV(2) N by auto then have "U∈T∨(U∩V=(⋃T-B)∩V∧(⋃T-B)∈(CoFinite (⋃T)))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto then have "U∈T∨(U∩V=(⋃T-B)∩V∧(⋃T-B)∈T)" using assms(1) T1_cocardinal_coarser by auto with UV(2) have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } ultimately have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto } ultimately show ?thesis unfolding IsATopology_def by auto qed text{*The previous construction preserves anti-hyperconnectedness.*} theorem (in topology0) COF_comp_antiHConn: assumes "T{is anti-}IsHConnected" "¬(⋃T≺nat)" shows "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T) {is anti-}IsHConnected" proof- have N:"⋃T∉(⋃T)" using mem_not_refl by auto from assms(1) have T1:"T{is T⇩_{1}}" using anti_HConn_imp_T1 by auto have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"] union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T" by auto ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"] tot1 unfolding Cofinite_def by auto moreover { assume "⋃T=0" with assms(2) have "¬(0≺nat)" by auto then have "False" unfolding lesspoll_def using empty_lepollI eqpoll_0_is_0 eqpoll_sym by auto } then have "⋃T≠0" by auto with N have Not:"¬(⋃T⊆{⋃T})" by auto { assume "{⋃T}∪⋃T={⋃T}" moreover have "⋃T⊆{⋃T}∪⋃T" by auto ultimately have "⋃T⊆{⋃T}" by auto with Not have "False" by auto } then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto { fix A assume AS:"A⊆⋃T" "(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A) {is hyperconnected}" from AS(1,2) have e0:"((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A=(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}⋃T){restricted to}A" using subspace_of_subspace[of "A""⋃T""((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)"] TOT by auto have e1:"(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}(⋃T))=((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T)∪(T{restricted to}⋃T)" unfolding RestrictedTo_def by auto { fix A assume "A∈T{restricted to}⋃T" then obtain B where "B∈T""A=B∩⋃T" unfolding RestrictedTo_def by auto then have "A=B" by auto with `B∈T` have "A∈T" by auto } then have "T{restricted to}⋃T⊆T" by auto moreover { fix A assume "A∈T" then have "⋃T∩A=A" by auto with `A∈T` have "A∈T{restricted to}⋃T" unfolding RestrictedTo_def by auto } ultimately have "T{restricted to}⋃T=T" by auto moreover { fix A assume "A∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T" then obtain B where "B∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}""⋃T∩B=A" unfolding RestrictedTo_def by auto then have "B∈({one-point compactification of}(CoFinite (⋃T)))""⋃T∩B=A" by auto then have "A∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T" unfolding RestrictedTo_def by auto then have "A∈(CoFinite (⋃T))" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]] union_cocardinal unfolding Cofinite_def by auto with T1 have "A∈T" using T1_cocardinal_coarser by auto } then have "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T⊆T" by auto moreover note e1 ultimately have "((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T) {restricted to} (⋃T)) =T" by auto with e0 have "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A=T{restricted to}A" by auto with assms(1) AS have "A{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto } then have reg:"∀A∈Pow(⋃T). ((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A) {is hyperconnected}) ⟶(A{is in the spectrum of}IsHConnected)" by auto have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto then have P:"⋃T∈((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)" by auto { fix B assume sub:"B∈Pow(⋃T ∪{⋃T})" and hyp:"((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B) {is hyperconnected})" from P have subop:"⋃T∩B∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" unfolding RestrictedTo_def by auto with hyp have hypSub:"((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B){restricted to}(⋃T∩B)){is hyperconnected}" using topology0.open_subspace_hyperconn topology0.Top_1_L4 COF_comp_is_top[OF T1 assms(2)] unfolding topology0_def by auto from sub TOT have "B ⊆ ⋃(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T)" by auto then have "(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}(⋃T∩B))=(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B){restricted to}(⋃T∩B)" using subspace_of_subspace[of "⋃T∩B""B""((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)"] by auto with hypSub have "((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T) {restricted to} (⋃T ∩ B)){is hyperconnected}" by auto with reg have "(⋃T∩B){is in the spectrum of}IsHConnected" by auto then have le:"⋃T∩B≲1" using HConn_spectrum by auto { fix x assume x:"x∈⋃T∩B" with le have sing:"⋃T∩B={x}" using lepoll_1_is_sing by auto { fix y assume y:"y∈B" then have "y∈⋃T ∪{⋃T}" using sub by auto with y have "y∈⋃T∩B∨y=⋃T" by auto with sing have "y=x∨y=⋃T" by auto } then have "B⊆{x,⋃T}" by auto with x have disj:"B={x}∨B={x,⋃T}" by auto { assume "⋃T∈B" with disj have B:"B={x,⋃T}" by auto from sing subop have singOp:"{x}∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" by auto have "{x}{is closed in}(CoFinite ⋃T)" using topology0.T1_iff_singleton_closed[OF topology0_CoCardinal[OF InfCard_nat]] cocardinal_is_T1[OF InfCard_nat] x union_cocardinal unfolding Cofinite_def by auto moreover have "Finite({x})" by auto then have spec:"{x}{is in the spectrum of} (λT. (⋃T) {is compact in}T)" using compact_spectrum by auto have "((CoFinite ⋃T){restricted to}{x}){is a topology}""⋃((CoFinite ⋃T){restricted to}{x})={x}" using topology0.Top_1_L4[OF topology0_CoCardinal[OF InfCard_nat]] unfolding RestrictedTo_def Cofinite_def using x union_cocardinal by auto with spec have "{x}{is compact in}((CoFinite ⋃T){restricted to}{x})" unfolding Spec_def by auto then have "{x}{is compact in}(CoFinite ⋃T)" using compact_subspace_imp_compact by auto moreover note x ultimately have "{⋃T}∪(⋃T-{x})∈{one-point compactification of}(CoFinite (⋃T))" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto moreover { assume A:"{⋃T}∪(⋃T-{x})={⋃T}" { fix y assume P:"y∈⋃T-{x}" then have "y∈{⋃T}∪(⋃T-{x})" by auto then have "y=⋃T" using A by auto with N P have "False" by auto } then have "⋃T-{x}=0" by auto with x have "⋃T={x}" by auto then 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 then have "False" using assms(2) by auto } ultimately have "{⋃T}∪(⋃T-{x})∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto then have "{⋃T}∪(⋃T-{x})∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T))" by auto then have "B∩({⋃T}∪(⋃T-{x}))∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" unfolding RestrictedTo_def by auto moreover have "B∩({⋃T}∪(⋃T-{x}))={⋃T}" using B by auto ultimately have "{⋃T}∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" by auto with singOp hyp N x have "False" unfolding IsHConnected_def by auto } with disj have "B={x}" by auto then have "B≈1" using singleton_eqpoll_1 by auto then have "B≲1" using eqpoll_imp_lepoll by auto } then have "⋃T∩B≠0⟶B≲1" by blast moreover { assume "⋃T∩B=0" with sub have "B⊆{⋃T}" by auto then have "B≲{⋃T}" using subset_imp_lepoll by auto then have "B≲1" using singleton_eqpoll_1 lepoll_eq_trans by auto } ultimately have "B≲1" by auto then have "B{is in the spectrum of}IsHConnected" using HConn_spectrum by auto } then show ?thesis unfolding antiProperty_def using TOT by auto qed text{*The previous construction, applied to a densely ordered topology, gives the desired counterexample. What happends is that every neighbourhood of @{text "⋃T"} is dense; because there are no finite open sets, and hence meets every non-empty open set. In conclusion, @{text "⋃T"} cannot be separated from other points by disjoint open sets.*} text{*Every open set that contains @{text "⋃T"} is dense, when considering the order topology in a densely ordered set with more than two points.*} theorem neigh_infPoint_dense: fixes T X r defines T_def:"T ≡ (OrdTopology X r)" assumes "IsLinOrder(X,r)" "X{is dense with respect to}r" "∃x y. x≠y∧x∈X∧y∈X" "U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" "⋃T∈U" "V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" "V≠0" shows "U∩V≠0" proof have N:"⋃T∉(⋃T)" using mem_not_refl by auto have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"] union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T" by auto ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"] tot1 unfolding Cofinite_def by auto moreover { assume "⋃T=0" then have "X=0" unfolding T_def using union_ordtopology[OF assms(2)] assms(4) by auto then have "False" using assms(4) by auto } then have "⋃T≠0" by auto with N have Not:"¬(⋃T⊆{⋃T})" by auto { assume "{⋃T}∪⋃T={⋃T}" moreover have "⋃T⊆{⋃T}∪⋃T" by auto ultimately have "⋃T⊆{⋃T}" by auto with Not have "False" by auto } then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto assume A:"U∩V=0" with assms(6) have NN:"⋃T∉V" by auto with assms(7) have "V∈(CoFinite ⋃T)∪T" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto moreover have "T{is T⇩_{2}}" unfolding T_def using order_top_T2[OF assms(2)] assms(4) by auto then have T1:"T{is T⇩_{1}}" using T2_is_T1 by auto ultimately have VopT:"V∈T" using topology0.T1_cocardinal_coarser[OF topology0_ordtopology(1)[OF assms(2)]] unfolding T_def by auto from A assms(7) have "V⊆⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)-U" by auto then have "V⊆({⋃T}∪⋃T)-U" using TOT by auto then have "V⊆(⋃T)-U" using NN by auto from N have "U∉T" using assms(6) by auto then have "U∉(CoFinite ⋃T)∪T" using T1 topology0.T1_cocardinal_coarser[OF topology0_ordtopology(1)[OF assms(2)]] unfolding T_def using union_cocardinal union_ordtopology[OF assms(2)] assms(4) by auto with assms(5,6) obtain B where U:"U={⋃T}∪(⋃T-B)" "B{is closed in}(CoFinite ⋃T)" "B≠⋃T" unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto then have "U={⋃T}∪(⋃T-B)" "B=⋃T ∨ B≺nat" "B≠⋃T" using closed_sets_cocardinal unfolding Cofinite_def by auto then have "U={⋃T}∪(⋃T-B)" "B≺nat" by auto with N have "⋃T-U=⋃T-(⋃T-B)" by auto then have "⋃T-U=B" using U(2) unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto with `B≺nat` have "Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto with `V⊆(⋃T)-U` have "Finite(V)" using subset_Finite by auto from assms(8) obtain v where "v∈V" by auto with VopT have "∃R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪{RightRayX(X, r, b) . b ∈ X}. R ⊆ V ∧ v ∈ R" using point_open_base_neigh[OF Ordtopology_is_a_topology(2)[OF assms(2)]] unfolding T_def by auto then obtain R where R_def:"R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪{RightRayX(X, r, b) . b ∈ X}" "R⊆V" "v∈R" by blast moreover { assume "R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X}" then obtain b c where lim:"b∈X""c∈X""R=IntervalX(X, r, b, c)" by auto with `v∈R` have " ¬ Finite(R)" using dense_order_inf_intervals[OF assms(2) _ _ _ assms(3)] by auto with `R⊆V` `Finite(V)` have "False" using subset_Finite by auto } moreover { assume "R∈{LeftRayX(X, r, b) . b ∈ X}" then obtain b where lim:"b∈X""R=LeftRayX(X, r, b)" by auto with `v∈R` have " ¬ Finite(R)" using dense_order_inf_lrays[OF assms(2) _ _ assms(3)] by auto with `R⊆V` `Finite(V)` have "False" using subset_Finite by auto } moreover { assume "R∈{RightRayX(X, r, b) . b ∈ X}" then obtain b where lim:"b∈X""R=RightRayX(X, r, b)" by auto with `v∈R` have " ¬ Finite(R)" using dense_order_inf_rrays[OF assms(2)_ _ assms(3)] by auto with `R⊆V` `Finite(V)` have "False" using subset_Finite by auto } ultimately show "False" by auto qed text{*A densely ordered set with more than one point gives an order topology. Applying the previous construction to this topology we get a non locally-Hausdorff space.*} theorem OPComp_cofinite_dense_order_not_loc_T2: fixes T X r defines T_def:"T ≡ (OrdTopology X r)" assumes "IsLinOrder(X,r)" "X{is dense with respect to}r" "∃x y. x≠y∧x∈X∧y∈X" shows "¬((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩_{2}})" proof have N:"⋃T∉(⋃T)" using mem_not_refl by auto have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"] union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T" by auto ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"] tot1 unfolding Cofinite_def by auto moreover { assume "⋃T=0" then have "X=0" unfolding T_def using union_ordtopology[OF assms(2)] assms(4) by auto then have "False" using assms(4) by auto } then have "⋃T≠0" by auto with N have Not:"¬(⋃T⊆{⋃T})" by auto { assume "{⋃T}∪⋃T={⋃T}" moreover have "⋃T⊆{⋃T}∪⋃T" by auto ultimately have "⋃T⊆{⋃T}" by auto with Not have "False" by auto } then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto have T1:"T{is T⇩_{1}}" using order_top_T2[OF assms(2,4)] T2_is_T1 unfolding T_def by auto moreover from assms(4) obtain b c where B:"b∈X""c∈X""b≠c" by auto { assume "⟨b,c⟩∉r" with assms(2) have "⟨c,b⟩∈r" unfolding IsLinOrder_def IsTotal_def using `b∈X``c∈X` by auto with assms(3) B obtain z where "z∈X-{b,c}""⟨c,z⟩∈r""⟨z,b⟩∈r" unfolding IsDense_def by auto then have "IntervalX(X,r,c,b)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto then have "¬(Finite(IntervalX(X,r,c,b)))" using dense_order_inf_intervals[OF assms(2) _ `c∈X``b∈X` assms(3)] by auto moreover have "IntervalX(X,r,c,b)⊆X" unfolding IntervalX_def by auto ultimately have "¬(Finite(X))" using subset_Finite by auto then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto } moreover { assume "⟨b,c⟩∈r" with assms(3) B obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" unfolding IsDense_def by auto then have "IntervalX(X,r,b,c)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto then have "¬(Finite(IntervalX(X,r,b,c)))" using dense_order_inf_intervals[OF assms(2) _ `b∈X``c∈X` assms(3)] by auto moreover have "IntervalX(X,r,b,c)⊆X" unfolding IntervalX_def by auto ultimately have "¬(Finite(X))" using subset_Finite by auto then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto } ultimately have "¬(X≺nat)" by auto with T1 have top:"(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is a topology}" using topology0.COF_comp_is_top[OF topology0_ordtopology[OF assms(2)]] unfolding T_def using union_ordtopology[OF assms(2,4)] by auto assume "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩_{2}}" moreover have "⋃T∈⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" using TOT by auto moreover have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" using top unfolding IsATopology_def by auto ultimately have "∃c∈Pow(⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)). ⋃T ∈ Interior(c, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T) ∧ ((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} c) {is T⇩_{2}}" unfolding IsLocallyT2_def IsLocally_def[OF top] by auto then obtain C where C:"C⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" "⋃T ∈ Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)" and T2:"((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C) {is T⇩_{2}}" by auto have sub:"Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)⊆C" using topology0.Top_2_L1 top unfolding topology0_def by auto have "(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}C){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))=((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))" using subspace_of_subspace[OF sub C(1)] by auto moreover have "(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))⊆C" unfolding RestrictedTo_def by auto with C(1) have "(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))=C" unfolding RestrictedTo_def by auto with sub have pp:"Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)∈Pow(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))" by auto ultimately have T2_2:"(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))){is T⇩_{2}}" using T2_here[OF T2 pp] by auto have top2:"(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))){is a topology}" using topology0.Top_1_L4 top unfolding topology0_def by auto from C(2) pp have p1:"⋃T∈⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))" unfolding RestrictedTo_def by auto from top topology0.Top_2_L2 have intOP:"(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding topology0_def by auto { fix x assume "x≠⋃T" "x∈⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))" with p1 have "∃U∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))). ∃V∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))). x∈U∧⋃T∈V∧U∩V=0" using T2_2 unfolding isT2_def by auto then obtain U V where UV:"U∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))" "V∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))" "U≠0""⋃T∈V""U∩V=0" by auto from UV(1) obtain UC where "U=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩UC""UC∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))" unfolding RestrictedTo_def by auto with top intOP have Uop:"U∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding IsATopology_def by auto from UV(2) obtain VC where "V=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩VC""VC∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))" unfolding RestrictedTo_def by auto with top intOP have "V∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding IsATopology_def by auto with UV(3-5) Uop neigh_infPoint_dense[OF assms(2-4),of "V""U"] union_ordtopology[OF assms(2,4)] have "False" unfolding T_def by auto } then have "⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))⊆{⋃T}" by auto with p1 have "⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))={⋃T}" by auto with top2 have "{⋃T}∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))" unfolding IsATopology_def by auto then obtain W where UT:"{⋃T}=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩W""W∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding RestrictedTo_def by auto from this(2) have "(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩W∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" using intOP top unfolding IsATopology_def by auto with UT(1) have "{⋃T}∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" by auto then have "{⋃T}∈T" by auto with N show "False" by auto qed text{*This topology, from the previous result, gives a counter-example for anti-hyperconnected implies locally-$T_2$.*} theorem antiHConn_not_imp_loc_T2: fixes T X r defines T_def:"T ≡ (OrdTopology X r)" assumes "IsLinOrder(X,r)" "X{is dense with respect to}r" "∃x y. x≠y∧x∈X∧y∈X" shows "¬((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩_{2}})" and "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is anti-}IsHConnected" using OPComp_cofinite_dense_order_not_loc_T2[OF assms(2-4)] dense_order_infinite[OF assms(2-4)] union_ordtopology[OF assms(2,4)] topology0.COF_comp_antiHConn[OF topology0_ordtopology[OF assms(2)] topology0.T2_imp_anti_HConn[OF topology0_ordtopology[OF assms(2)] order_top_T2[OF assms(2,4)]]] unfolding T_def by auto text{*Let's prove that $T_2$ spaces are locally-$T_2$, but that there are locally-$T_2$ spaces which aren't $T_2$. In conclusion $T_2\Rightarrow$ locally -$T_2\Rightarrow$ anti-hyperconnected; all implications proper.*} theorem(in topology0) T2_imp_loc_T2: assumes "T{is T⇩_{2}}" shows "T{is locally-T⇩_{2}}" proof- { fix x assume "x∈⋃T" { fix b assume b:"b∈T""x∈b" then have "(T{restricted to}b){is T⇩_{2}}" using T2_here assms by auto moreover from b have "x∈int(b)" using Top_2_L3 by auto ultimately have "∃c∈Pow(b). x∈int(c)∧(T{restricted to}c){is T⇩_{2}}" by auto } then have "∀b∈T. x∈b ⟶(∃c∈Pow(b). x∈int(c)∧(T{restricted to}c){is T⇩_{2}})" by auto } then show ?thesis unfolding IsLocallyT2_def IsLocally_def[OF topSpaceAssum] by auto qed text{*If there is a closed singleton, then we can consider a topology that makes this point doble.*} theorem(in topology0) doble_point_top: assumes "{m}{is closed in}T" shows "(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is a topology}" proof- { fix M assume M:"M⊆T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" let ?MT="{V∈M. V∈T}" let ?Mm="{V∈M. V∉T}" have unm:"⋃M=(⋃?MT)∪(⋃?Mm)" by auto have tt:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto { assume "?Mm=0" then have "⋃?Mm=0" by auto with unm have "⋃M=(⋃?MT)" by auto with tt have "⋃M∈T" by auto then have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } moreover { assume AS:"?Mm≠0" then obtain V where V:"V∈M""V∉T" by auto with M have "V∈{(U - {m}) ∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast then obtain U W where U:"V=(U-{m})∪{⋃T}∪W" "U∈T""m∈U" "W∈T" by auto let ?U="{⟨V,W⟩∈T×T. m∈V∧ (V-{m})∪{⋃T}∪W∈?Mm}" let ?fU="{fst(B). B∈?U}" let ?sU="{snd(B). B∈?U}" have "?fU⊆T""?sU⊆T" by auto then have P:"⋃?fU∈T""⋃?sU∈T" using topSpaceAssum unfolding IsATopology_def by auto moreover have "⟨U,W⟩∈?U" using U V by auto then have "m∈⋃?fU" by auto ultimately have s:"⟨⋃?fU,⋃?sU⟩∈{V∈T. m∈V}×T" by auto moreover have r:"∀S. ∀R. S∈{V∈T. m∈V}⟶ R∈T⟶(S-{m})∪{⋃T}∪R∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto ultimately have "(⋃?fU-{m})∪{⋃T}∪⋃?sU∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto { fix v assume "v∈⋃?Mm" then obtain V where v:"v∈V""V∈?Mm" by auto then have V:"V∈M""V∉T" by auto with M have "V∈{U - {m} ∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast then obtain U W where U:"V=(U-{m})∪{⋃T}∪W" "U∈T""m∈U" "W∈T" by auto with v(1) have "v∈(U-{m})∪{⋃T}∪W" by auto then have "v∈U-{m}∨v=⋃T∨v∈W" by auto then have "(v∈U∧v≠m)∨v=⋃T∨v∈W" by auto moreover from U V have "⟨U,W⟩∈?U" by auto ultimately have "v∈((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by auto } then have "⋃?Mm⊆((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by blast moreover { fix v assume v:"v∈((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" { assume "v=⋃T" then have "v∈(U-{m})∪{⋃T}∪W" by auto with `⟨U,W⟩∈?U` have "v∈⋃?Mm" by auto } moreover { assume "v≠⋃T""v∉⋃?sU" with v have "v∈((⋃?fU)-{m})" by auto then have "(v∈⋃?fU∧v≠m)" by auto then obtain W where "(v∈W∧W∈?fU∧v≠m)" by auto then have "v∈(W-{m})∪{⋃T}" "W∈?fU" by auto then obtain B where "fst(B)=W" "B∈?U" "v∈(W-{m})∪{⋃T}" by blast then have "v∈⋃?Mm" by auto } ultimately have "v∈⋃?Mm" by auto } then have "((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)⊆⋃?Mm" by auto ultimately have "⋃?Mm=((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by auto then have "⋃M=((⋃?fU)-{m})∪{⋃T}∪((⋃?sU)∪(⋃?MT))" using unm by auto moreover from P tt have "(⋃?sU)∪(⋃?MT)∈T" using topSpaceAssum union_open[OF topSpaceAssum, of "{⋃?sU,⋃?MT}"] by auto with s have "⟨⋃?fU,(⋃?sU)∪(⋃?MT)⟩∈{V∈T. m∈V}×T" by auto then have "((⋃?fU)-{m})∪{⋃T}∪((⋃?sU)∪(⋃?MT))∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using r by auto ultimately have "⋃M∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } ultimately have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } then have "∀M∈Pow(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ⋃M∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto moreover { fix A B assume ass:"A∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}""B∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" { assume A:"A∈T" { assume "B∈T" with A have "A∩B∈T" using topSpaceAssum unfolding IsATopology_def by auto } moreover { assume "B∉T" with ass(2) have "B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain U W where U:"U∈T""m∈U""W∈T""B=(U-{m})∪{⋃T}∪W" by auto moreover from A mem_not_refl have "⋃T∉A" by auto ultimately have "A∩B=A∩((U-{m})∪W)" by auto then have eq:"A∩B=(A∩(U-{m}))∪(A∩W)" by auto have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto with U(1) have O:"U∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def by auto have "U∩(⋃T-{m})=U-{m}" using U(1) by auto with O have "U-{m}∈T" by auto with A have "(A∩(U-{m}))∈T" using topSpaceAssum unfolding IsATopology_def by auto moreover from A U(3) have "A∩W∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have "(A∩(U-{m}))∪(A∩W)∈T" using union_open[OF topSpaceAssum, of "{A∩(U-{m}),A∩W}"] by auto with eq have "A∩B∈T" by auto } ultimately have "A∩B∈T" by auto } moreover { assume "A∉T" with ass(1) have A:"A∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto { assume B:"B∈T" from A obtain U W where U:"U∈T""m∈U""W∈T""A=(U-{m})∪{⋃T}∪W" by auto moreover from B mem_not_refl have "⋃T∉B" by auto ultimately have "A∩B=((U-{m})∪W)∩B" by auto then have eq:"A∩B=((U-{m})∩B)∪(W∩B)" by auto have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto with U(1) have O:"U∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def by auto have "U∩(⋃T-{m})=U-{m}" using U(1) by auto with O have "U-{m}∈T" by auto with B have "((U-{m})∩B)∈T" using topSpaceAssum unfolding IsATopology_def by auto moreover from B U(3) have "W∩B∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have "((U-{m})∩B)∪(W∩B)∈T" using union_open[OF topSpaceAssum, of "{((U-{m})∩B),(W∩B)}"] by auto with eq have "A∩B∈T" by auto } moreover { assume "B∉T" with ass(2) have "B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain U W where U:"U∈T""m∈U""W∈T""B=(U-{m})∪{⋃T}∪W" by auto moreover from A obtain UA WA where UA:"UA∈T""m∈UA""WA∈T""A=(UA-{m})∪{⋃T}∪WA" by auto ultimately have "A∩B=(((UA-{m})∪WA)∩((U-{m})∪W))∪{⋃T}" by auto then have eq:"A∩B=((UA-{m})∩(U-{m}))∪(WA∩(U-{m}))∪((UA-{m})∩W)∪(WA∩W)∪{⋃T}" by auto have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto with U(1) UA(1) have O:"U∩(⋃T-{m})∈T""UA∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def by auto have "U∩(⋃T-{m})=U-{m}""UA∩(⋃T-{m})=UA-{m}" using U(1) UA(1) by auto with O have OO:"U-{m}∈T""UA-{m}∈T" by auto then have "((UA-{m})∩(U-{m}))=UA∩U-{m}" by auto moreover have "UA∩U∈T""m∈UA∩U" using U(1,2) UA(1,2) topSpaceAssum unfolding IsATopology_def by auto moreover from OO U(3) UA(3) have TT:"WA∩(U-{m})∈T""(UA-{m})∩W∈T""WA∩W∈T" using topSpaceAssum unfolding IsATopology_def by auto from TT(2,3) have "((UA-{m})∩W)∪(WA∩W)∈T" using union_open[OF topSpaceAssum, of "{(UA-{m})∩W,WA∩W}"] by auto with TT(1) have "(WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W))∈T" using union_open[OF topSpaceAssum, of "{WA∩(U-{m}),((UA-{m})∩W)∪(WA∩W)}"] by auto ultimately have "A∩B=(UA∩U-{m})∪{⋃T}∪((WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W)))" "(WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W))∈T" "UA∩U∈{V∈T. m∈V}" using eq by auto then have "∃W∈T. A∩B=(UA∩U-{m})∪{⋃T}∪W" "UA∩U∈{V∈T. m∈V}" by auto then have "A∩B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } ultimately have "A∩B∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } ultimately have "A∩B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto } then have "∀A∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}. ∀B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}. A∩B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast ultimately show ?thesis unfolding IsATopology_def by auto qed text{*The previous topology is defined over a set with one more point.*} lemma(in topology0) union_doublepoint_top: assumes "{m}{is closed in}T" shows "⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})=⋃T ∪{⋃T}" proof { fix x assume "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" then obtain R where x:"x∈R""R∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast { assume "R∈T" with x(1) have "x∈⋃T" by auto } moreover { assume "R∉T" with x(2) have "R∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain U W where "R=(U-{m})∪{⋃T}∪W""W∈T""U∈T""m∈U" by auto with x(1) have "x=⋃T∨x∈⋃T" by auto } ultimately have "x∈⋃T ∪{⋃T}" by auto } then show "⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})⊆⋃T ∪{⋃T}" by auto { fix x assume "x∈⋃T ∪{⋃T}" then have dis:"x∈⋃T∨x=⋃T" by auto { assume "x∈⋃T" then have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto } moreover { assume "x∉⋃T" with dis have "x=⋃T" by auto moreover from assms have "⋃T-{m}∈T""m∈⋃T" unfolding IsClosed_def by auto moreover have "0∈T" using empty_open topSpaceAssum by auto ultimately have "x∈(⋃T-{m})∪{⋃T}∪0" "(⋃T-{m})∪{⋃T}∪0∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using union_open[OF topSpaceAssum] by auto then have "x∈(⋃T-{m})∪{⋃T}∪0" "(⋃T-{m})∪{⋃T}∪0∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by blast } ultimately have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto } then show "⋃T ∪{⋃T}⊆⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto qed text{*In this topology, the previous topological space is an open subspace.*} theorem(in topology0) open_subspace_double_point: assumes "{m}{is closed in}T" shows "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T" and "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" proof- have N:"⋃T∉⋃T" using mem_not_refl by auto { fix x assume "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" then obtain U where U:"U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})""x=⋃T∩U" unfolding RestrictedTo_def by blast { assume "U∉T" with U(1) have "U∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain V W where VW:"U=(V-{m})∪{⋃T}∪W""V∈T""m∈V""W∈T" by auto with N U(2) have x:"x=(V-{m})∪W" by auto have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto then have "V∩(⋃T-{m})∈T" using VW(2) topSpaceAssum unfolding IsATopology_def by auto moreover have "V-{m}=V∩(⋃T-{m})" using VW(2,3) by auto ultimately have "V-{m}∈T" by auto with VW(4) have "(V-{m})∪W∈T" using union_open[OF topSpaceAssum, of "{V-{m},W}"] by auto with x have "x∈T" by auto } moreover { assume A:"U∈T" with U(2) have "x=U" by auto with A have "x∈T" by auto } ultimately have "x∈T" by auto } then have "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T⊆T" by auto moreover { fix x assume x:"x∈T" then have "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto moreover from x have "⋃T∩x=x" by auto ultimately have "∃M∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ⋃T∩M=x" by blast then have "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" unfolding RestrictedTo_def by auto } ultimately show "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T" by auto have P:"⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto then show "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto qed text{*The previous topology construction applied to a $T_2$ non-discrite space topology, gives a counter-example to: Every locally-$T_2$ space is $T_2$.*} text{*If there is a singleton which is not open, but closed; then the construction on that point is not $T_2$.*} theorem(in topology0) loc_T2_imp_T2_counter_1: assumes "{m}∉T" "{m}{is closed in}T" shows "¬((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is T⇩_{2}})" proof assume ass:"(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is T⇩_{2}}" then have tot1:"⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})=⋃T ∪{⋃T}" using union_doublepoint_top assms(2) by auto have "m≠⋃T" using mem_not_refl assms(2) unfolding IsClosed_def by auto moreover from ass tot1 have "∀x y. x∈⋃T ∪{⋃T} ∧ y∈⋃T ∪{⋃T}∧x≠y ⟶ (∃𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ∃𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). x∈𝔘∧y∈𝔙∧𝔘∩𝔙=0)" unfolding isT2_def by auto moreover from assms(2) have "m∈⋃T ∪{⋃T}" unfolding IsClosed_def by auto moreover have "⋃T∈⋃T ∪{⋃T}" by auto ultimately have "∃𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ∃𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). m∈𝔘∧⋃T∈𝔙∧𝔘∩𝔙=0" by auto then obtain 𝔘 𝔙 where UV:"𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" "𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})""m∈𝔘""⋃T∈𝔙""𝔘∩𝔙=0" using tot1 by blast then have "⋃T∉𝔘" by auto with UV(1) have P:"𝔘∈T" by auto { assume "𝔙∈T" then have "𝔙⊆⋃T" by auto with UV(4) have "⋃T∈⋃T" using tot1 by auto then have "False" using mem_not_refl by auto } with UV(2) have "𝔙∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then obtain U W where V:"𝔙=(U-{m})∪{⋃T}∪W" "U∈T""m∈U""W∈T" by auto from V(2,3) P have int:"U∩𝔘∈T""m∈U∩𝔘" using UV(3) topSpaceAssum unfolding IsATopology_def by auto have "(U∩𝔘-{m})⊆𝔘" "(U∩𝔘-{m})⊆𝔙" using V(1) by auto then have "(U∩𝔘-{m})=0" using UV(5) by auto with int(2) have "U∩𝔘={m}" by auto with int(1) assms(1) show "False" by auto qed text{*This topology is locally-$T_2$.*} theorem(in topology0) loc_T2_imp_T2_counter_2: assumes "{m}∉T" "m∈⋃T" "T{is T⇩_{2}}" shows "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is locally-T⇩_{2}}" proof- from assms(3) have "T{is T⇩_{1}}" using T2_is_T1 by auto with assms(2) have mc:"{m}{is closed in}T" using T1_iff_singleton_closed by auto have N:"⋃T∉⋃T" using mem_not_refl by auto have res:"(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T" and P:"⋃T∈T" and Q:"⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using open_subspace_double_point mc topSpaceAssum unfolding IsATopology_def by auto { fix A assume ass:"A∈⋃T ∪{⋃T}" { assume "A≠⋃T" with ass have "A∈⋃T" by auto with Q res assms(3) have "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})∧ A∈⋃T ∧ (((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T){is T⇩_{2}})" by auto then have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩_{2}})" by blast } moreover { assume A:"A=⋃T" have "⋃T∈T""m∈⋃T""0∈T" using assms(2) empty_open[OF topSpaceAssum] unfolding IsClosed_def using P by auto then have "(⋃T-{m})∪{⋃T}∪0∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then have opp:"(⋃T-{m})∪{⋃T}∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto { fix A1 A2 assume points:"A1∈(⋃T-{m})∪{⋃T}""A2∈(⋃T-{m})∪{⋃T}""A1≠A2" from points(1,2) have notm:"A1≠m""A2≠m" using assms(2) unfolding IsClosed_def using mem_not_refl by auto { assume or:"A1∈⋃T""A2∈⋃T" with points(3) assms(3) obtain U V where UV:"U∈T""V∈T""A1∈U""A2∈V" "U∩V=0" unfolding isT2_def by blast from UV(1,2) have "U∩((⋃T-{m})∪{⋃T})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" "V∩((⋃T-{m})∪{⋃T})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def by auto moreover then have "U∩(⋃T-{m})=U∩((⋃T-{m})∪{⋃T})" "V∩(⋃T-{m})=V∩((⋃T-{m})∪{⋃T})" using UV(1,2) mem_not_refl[of "⋃T"] by auto ultimately have opUV:"U∩(⋃T-{m})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" "V∩(⋃T-{m})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" by auto moreover have "U∩(⋃T-{m})∩(V∩(⋃T-{m}))=0" using UV(5) by auto moreover from UV(3) or(1) notm(1) have "A1∈U∩(⋃T-{m})" by auto moreover from UV(4) or(2) notm(2) have "A2∈V∩(⋃T-{m})" by auto ultimately have "∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ A1∈U∩(⋃T-{m})∧A2∈V∧(U∩(⋃T-{m}))∩V=0" using exI[where x="V∩(⋃T-{m})" and P="λW. W∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧A1∈(U∩(⋃T-{m}))∧A2∈W∧(U∩(⋃T-{m}))∩W=0"] using opUV(2) by auto then have "∃U. U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧(∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ A1∈U∧A2∈V∧U∩V=0)" using exI[where x="U∩(⋃T-{m})" and P="λW. W∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧(∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ A1∈W∧A2∈V∧W∩V=0)"] using opUV(1) by auto then have "∃U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧A1∈U∧A2∈V∧U∩V=0)" by blast then have "∃U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" by blast } moreover { assume "A1∉⋃T" then have ig:"A1=⋃T" using points(1) by auto { assume "A2∉⋃T" then have "A2=⋃T" using points(2) by auto with points(3) ig have "False" by auto } then have igA2:"A2∈⋃T" by auto moreover have "m∈⋃T" using assms(2) unfolding IsClosed_def by auto moreover note notm(2) assms(3) ultimately obtain U V where UV:"U∈T""V∈T" "m∈U""A2∈V""U∩V=0" unfolding isT2_def by blast from UV(1,3) have "U∈{W∈T. m∈W}" by auto moreover have "0∈T" using empty_open topSpaceAssum by auto ultimately have "(U-{m})∪{⋃T}∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then have Uop:"(U-{m})∪{⋃T}∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto from UV(2) have Vop:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto from UV(1-3,5) have sub:"V⊆(⋃T-{m})∪{⋃T}" "((U-{m})∪{⋃T})⊆(⋃T-{m})∪{⋃T}" by auto from sub(1) have "V=((⋃T-{m})∪{⋃T})∩V" by auto then have VV:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def using Vop by blast moreover from sub(2) have "((U-{m})∪{⋃T})=((⋃T-{m})∪{⋃T})∩((U-{m})∪{⋃T})" by auto then have UU:"((U-{m})∪{⋃T})∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def using Uop by blast moreover from UV(2) have "((U-{m})∪{⋃T})∩V=(U-{m})∩V" using mem_not_refl by auto then have "((U-{m})∪{⋃T})∩V=0" using UV(5) by auto with UV(4) VV ig igA2 have "∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈(U-{m})∪{⋃T}∧A2∈V∧((U-{m})∪{⋃T})∩V=0" by auto with UU ig have "∃U. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" using exI[where x="((U-{m})∪{⋃T})" and P="λU. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)"] by auto then have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" by blast } moreover { assume "A2∉⋃T" then have ig:"A2=⋃T" using points(2) by auto { assume "A1∉⋃T" then have "A1=⋃T" using points(1) by auto with points(3) ig have "False" by auto } then have igA2:"A1∈⋃T" by auto moreover have "m∈⋃T" using assms(2) unfolding IsClosed_def by auto moreover note notm(1) assms(3) ultimately obtain U V where UV:"U∈T""V∈T" "m∈U""A1∈V""U∩V=0" unfolding isT2_def by blast from UV(1,3) have "U∈{W∈T. m∈W}" by auto moreover have "0∈T" using empty_open topSpaceAssum by auto ultimately have "(U-{m})∪{⋃T}∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto then have Uop:"(U-{m})∪{⋃T}∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto from UV(2) have Vop:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto from UV(1-3,5) have sub:"V⊆(⋃T-{m})∪{⋃T}" "((U-{m})∪{⋃T})⊆(⋃T-{m})∪{⋃T}" by auto from sub(1) have "V=((⋃T-{m})∪{⋃T})∩V" by auto then have VV:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def using Vop by blast moreover from sub(2) have "((U-{m})∪{⋃T})=((⋃T-{m})∪{⋃T})∩((U-{m})∪{⋃T})" by auto then have UU:"((U-{m})∪{⋃T})∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def using Uop by blast moreover from UV(2) have "V∩((U-{m})∪{⋃T})=V∩(U-{m})" using mem_not_refl by auto then have "V∩((U-{m})∪{⋃T})=0" using UV(5) by auto with UU UV(4) ig igA2 have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈V∧A2∈U∧V∩U=0" by auto with VV igA2 have "∃U. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" using exI[where x="V" and P="λU. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)"] by auto then have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" by blast } ultimately have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" by blast } then have "∀A1∈(⋃T-{m})∪{⋃T}. ∀A2∈(⋃T-{m})∪{⋃T}. A1≠A2 ⟶ (∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0))" by auto moreover have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))∩((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def by auto then have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃T ∪{⋃T})∩((⋃T-{m})∪{⋃T})" using union_doublepoint_top mc by auto then have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃T-{m})∪{⋃T}" by auto ultimately have "∀A1∈⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})). ∀A2∈⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})). A1≠A2 ⟶ (∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0))" by auto then have "((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})){is T⇩_{2}}" unfolding isT2_def by force with opp A have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩_{2}})" by blast } ultimately have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩_{2}})" by blast } then have "∀A∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ∃Z∈T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}. A ∈ Z ∧ ((T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}) {restricted to} Z) {is T⇩_{2}}" using union_doublepoint_top mc by auto with topology0.loc_T2 show "(T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}){is locally-T⇩_{2}}" unfolding topology0_def using doble_point_top mc by auto qed text{*There can be considered many more local properties, which; as happens with locally-$T_2$; can distinguish between spaces other properties cannot.*} end