(* 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(1) ‹?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(1) 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