(* 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 ‹Topology 9› theory Topology_ZF_9 imports Topology_ZF_2 Group_ZF_2 Topology_ZF_7 Topology_ZF_8 begin subsection‹Group of homeomorphisms› text‹This theory file deals with the fact the set homeomorphisms of a topological space into itself forms a group.› text‹First, we define the set of homeomorphisms.› definition "HomeoG(T) ≡ {f:⋃T→⋃T. IsAhomeomorphism(T,T,f)}" text‹The homeomorphisms are closed by composition.› lemma (in topology0) homeo_composition: assumes "f∈HomeoG(T)""g∈HomeoG(T)" shows "Composition(⋃T)`⟨f, g⟩∈HomeoG(T)" proof- from assms have fun:"f∈⋃T→⋃T""g∈⋃T→⋃T" and homeo:"IsAhomeomorphism(T,T,f)""IsAhomeomorphism(T,T,g)" unfolding HomeoG_def by auto from fun have "f O g∈⋃T→⋃T" using comp_fun by auto moreover from homeo have bij:"f∈bij(⋃T,⋃T)""g∈bij(⋃T,⋃T)" and cont:"IsContinuous(T,T,f)""IsContinuous(T,T,g)" and contconv: "IsContinuous(T,T,converse(f))""IsContinuous(T,T,converse(g))" unfolding IsAhomeomorphism_def by auto from bij have "f O g∈bij(⋃T,⋃T)" using comp_bij by auto moreover from cont have "IsContinuous(T,T,f O g)" using comp_cont by auto moreover have "converse(f O g)=converse(g) O converse(f)" using converse_comp by auto with contconv have "IsContinuous(T,T,converse(f O g))" using comp_cont by auto ultimately have "f O g∈HomeoG(T)" unfolding HomeoG_def IsAhomeomorphism_def by auto then show ?thesis using func_ZF_5_L2 fun by auto qed text‹The identity function is a homeomorphism.› lemma (in topology0) homeo_id: shows "id(⋃T)∈HomeoG(T)" proof- have "converse(id(⋃T)) O id(⋃T)=id(⋃T)" using left_comp_inverse id_bij by auto then have "converse(id(⋃T))=id(⋃T)" using right_comp_id by auto then show ?thesis unfolding HomeoG_def IsAhomeomorphism_def using id_cont id_type id_bij by auto qed text‹The homeomorphisms form a monoid and its neutral element is the identity.› theorem (in topology0) homeo_submonoid: shows "IsAmonoid(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))" "TheNeutralElement(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))=id(⋃T)" proof- have cl:"HomeoG(T) {is closed under} Composition(⋃T)" unfolding IsOpClosed_def using homeo_composition by auto moreover have sub:"HomeoG(T)⊆⋃T→⋃T" unfolding HomeoG_def by auto moreover have ne:"TheNeutralElement(⋃T→⋃T, Composition(⋃T))∈HomeoG(T)" using homeo_id Group_ZF_2_5_L2(2) by auto ultimately show "IsAmonoid(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))" using Group_ZF_2_5_L2(1) monoid0.group0_1_T1 unfolding monoid0_def by force from cl sub ne have "TheNeutralElement(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))=TheNeutralElement(⋃T→⋃T, Composition(⋃T))" using Group_ZF_2_5_L2(1) group0_1_L6 by blast moreover have "id(⋃T)=TheNeutralElement(⋃T→⋃T, Composition(⋃T))" using Group_ZF_2_5_L2(2) by auto ultimately show "TheNeutralElement(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))=id(⋃T)" by auto qed text‹The homeomorphisms form a group, with the composition.› theorem(in topology0) homeo_group: shows "IsAgroup(HomeoG(T),restrict(Composition(⋃T),HomeoG(T)×HomeoG(T)))" proof- { fix x assume AS:"x∈HomeoG(T)" then have surj:"x∈surj(⋃T,⋃T)" and bij:"x∈bij(⋃T,⋃T)" unfolding HomeoG_def IsAhomeomorphism_def bij_def by auto from bij have "converse(x)∈bij(⋃T,⋃T)" using bij_converse_bij by auto with bij have conx_fun:"converse(x)∈⋃T→⋃T""x∈⋃T→⋃T" unfolding bij_def inj_def by auto from surj have id:"x O converse(x)=id(⋃T)" using right_comp_inverse by auto from conx_fun have "Composition(⋃T)`⟨x,converse(x)⟩=x O converse(x)" using func_ZF_5_L2 by auto with id have "Composition(⋃T)`⟨x,converse(x)⟩=id(⋃T)" by auto moreover have "converse(x)∈HomeoG(T)" unfolding HomeoG_def using conx_fun(1) homeo_inv AS unfolding HomeoG_def by auto ultimately have "∃M∈HomeoG(T). Composition(⋃T)`⟨x,M⟩=id(⋃T)" by auto } then have "∀x∈HomeoG(T). ∃M∈HomeoG(T). Composition(⋃T)`⟨x,M⟩=id(⋃T)" by auto then show ?thesis using homeo_submonoid definition_of_group by auto qed subsection‹Examples computed› text‹As a first example, we show that the group of homeomorphisms of the cocardinal topology is the group of bijective functions.› theorem homeo_cocardinal: assumes "InfCard(Q)" shows "HomeoG(CoCardinal(X,Q))=bij(X,X)" proof from assms have n:"Q≠0" unfolding InfCard_def by auto then show "HomeoG(CoCardinal(X,Q)) ⊆ bij(X, X)" unfolding HomeoG_def IsAhomeomorphism_def using union_cocardinal by auto { fix f assume a:"f∈bij(X,X)" then have "converse(f)∈bij(X,X)" using bij_converse_bij by auto then have cinj:"converse(f)∈inj(X,X)" unfolding bij_def by auto from a have fun:"f∈X→X" unfolding bij_def inj_def by auto then have two:"two_top_spaces0((CoCardinal(X,Q)),(CoCardinal(X,Q)),f)" unfolding two_top_spaces0_def using union_cocardinal assms n CoCar_is_topology by auto { fix N assume "N{is closed in}(CoCardinal(X,Q))" then have N_def:"N=X ∨ (N∈Pow(X) ∧ N≺Q)" using closed_sets_cocardinal n by auto then have "restrict(converse(f),N)∈bij(N,converse(f)``N)" using cinj restrict_bij by auto then have "N≈f-``N" unfolding vimage_def eqpoll_def by auto then have "f-``N≈N" using eqpoll_sym by auto with N_def have "N=X ∨ (f-``N≺Q ∧ N∈Pow(X))" using eq_lesspoll_trans by auto with fun have "f-``N=X ∨ (f-``N≺Q ∧ (f-``N)∈Pow(X))" using func1_1_L3 func1_1_L4 by auto then have "f-``N {is closed in}(CoCardinal(X,Q))" using closed_sets_cocardinal n by auto } then have "∀N. N{is closed in}(CoCardinal(X,Q)) ⟶ f-``N {is closed in}(CoCardinal(X,Q))" by auto then have "IsContinuous((CoCardinal(X,Q)),(CoCardinal(X,Q)),f)" using two_top_spaces0.Top_ZF_2_1_L4 two_top_spaces0.Top_ZF_2_1_L3 two_top_spaces0.Top_ZF_2_1_L2 two by auto } then have "∀f∈bij(X,X). IsContinuous((CoCardinal(X,Q)),(CoCardinal(X,Q)),f)" by auto then have "∀f∈bij(X,X). IsContinuous((CoCardinal(X,Q)),(CoCardinal(X,Q)),f) ∧ IsContinuous((CoCardinal(X,Q)),(CoCardinal(X,Q)),converse(f))" using bij_converse_bij by auto then have "∀f∈bij(X,X). IsAhomeomorphism((CoCardinal(X,Q)),(CoCardinal(X,Q)),f)" unfolding IsAhomeomorphism_def using n union_cocardinal by auto then show "bij(X,X)⊆HomeoG((CoCardinal(X,Q)))" unfolding HomeoG_def bij_def inj_def using n union_cocardinal by auto qed text‹The group of homeomorphism of the excluded set is a direct product of the bijections on $X\setminus T$ and the bijections on $X\cap T$.› theorem homeo_excluded: shows "HomeoG(ExcludedSet(X,T))={f∈bij(X,X). f``(X-T)=(X-T)}" proof have sub1:"X-T⊆X" by auto { fix g assume "g∈HomeoG(ExcludedSet(X,T))" then have fun:"g:X→X" and bij:"g∈bij(X,X)" and hom:"IsAhomeomorphism((ExcludedSet(X,T)),(ExcludedSet(X,T)),g)" unfolding HomeoG_def using union_excludedset unfolding IsAhomeomorphism_def by auto { assume A:"g``(X-T)=X" and B:"X∩T≠0" have rfun:"restrict(g,X-T):X-T→X" using fun restrict_fun sub1 by auto moreover from A fun have "{g`aa. aa∈X-T}=X" using func_imagedef sub1 by auto then have "∀x∈X. x∈{g`aa. aa∈X-T}" by auto then have "∀x∈X. ∃aa∈X-T. x=g`aa" by auto then have "∀x∈X. ∃aa∈X-T. x=restrict(g,X-T)`aa" by auto with A have surj:"restrict(g,X-T)∈surj(X-T,X)" using rfun unfolding surj_def by auto from B obtain d where "d∈X""d∈T" by auto with bij have "g`d∈X" using apply_funtype unfolding bij_def inj_def by auto then obtain s where "restrict(g,X-T)`s=g`d""s∈X-T" using surj unfolding surj_def by blast then have "g`s=g`d" by auto with ‹d∈X›‹s∈X-T› have "s=d" using bij unfolding bij_def inj_def by auto then have "False" using ‹s∈X-T› ‹d∈T› by auto } then have "g``(X-T)=X ⟶ X∩T=0" by auto then have reg:"g``(X-T)=X ⟶ X-T=X" by auto then have "g``(X-T)=X ⟶ g``(X-T)=X-T" by auto then have "g``(X-T)=X ⟶ g∈{f∈bij(X,X). f``(X-T)=(X-T)}" using bij by auto moreover { fix gg assume A:"gg``(X-T)≠X" and hom2:"IsAhomeomorphism((ExcludedSet(X,T)),(ExcludedSet(X,T)),gg)" from hom2 have fun:"gg∈X→X" and bij:"gg∈bij(X,X)" unfolding IsAhomeomorphism_def bij_def inj_def using union_excludedset by auto have sub:"X-T⊆⋃(ExcludedSet(X,T))" using union_excludedset by auto with hom2 have "gg``(Interior(X-T,(ExcludedSet(X,T))))=Interior(gg``(X-T),(ExcludedSet(X,T)))" using int_top_invariant by auto moreover from sub1 have "Interior(X-T,(ExcludedSet(X,T)))=X-T" using interior_set_excludedset by auto ultimately have "gg``(X-T)=Interior(gg``(X-T),(ExcludedSet(X,T)))" by auto moreover have ss:"gg``(X-T)⊆X" using fun func1_1_L6(2) by auto then have "Interior(gg``(X-T),(ExcludedSet(X,T))) = (gg``(X-T))-T" using interior_set_excludedset A by auto ultimately have eq:"gg``(X-T)=(gg``(X-T))-T" by auto { assume "(gg``(X-T))∩T≠0" then obtain t where "t∈T" and im:"t∈gg``(X-T)" by blast then have "t∉(gg``(X-T))-T" by auto then have "False" using eq im by auto } then have "(gg``(X-T))∩T=0" by auto then have "gg``(X-T)⊆X-T" using ss by blast } then have "∀gg. gg``(X-T)≠X ∧ IsAhomeomorphism(ExcludedSet(X,T),ExcludedSet(X,T),gg)⟶ gg``(X-T)⊆X-T" by auto moreover from bij have conbij:"converse(g)∈bij(X,X)" using bij_converse_bij by auto then have confun:"converse(g)∈X→X" unfolding bij_def inj_def by auto { assume A:"converse(g)``(X-T)=X" and B:"X∩T≠0" have rfun:"restrict(converse(g),X-T):X-T→X" using confun restrict_fun sub1 by auto moreover from A confun have "{converse(g)`aa. aa∈X-T}=X" using func_imagedef sub1 by auto then have "∀x∈X. x∈{converse(g)`aa. aa∈X-T}" by auto then have "∀x∈X. ∃aa∈X-T. x=converse(g)`aa" by auto then have "∀x∈X. ∃aa∈X-T. x=restrict(converse(g),X-T)`aa" by auto with A have surj:"restrict(converse(g),X-T)∈surj(X-T,X)" using rfun unfolding surj_def by auto from B obtain d where "d∈X""d∈T" by auto with conbij have "converse(g)`d∈X" using apply_funtype unfolding bij_def inj_def by auto then obtain s where "restrict(converse(g),X-T)`s=converse(g)`d""s∈X-T" using surj unfolding surj_def by blast then have "converse(g)`s=converse(g)`d" by auto with ‹d∈X›‹s∈X-T› have "s=d" using conbij unfolding bij_def inj_def by auto then have "False" using ‹s∈X-T› ‹d∈T› by auto } then have "converse(g)``(X-T)=X ⟶ X∩T=0" by auto then have "converse(g)``(X-T)=X ⟶ X-T=X" by auto then have "converse(g)``(X-T)=X ⟶ g-``(X-T)=(X-T)" unfolding vimage_def by auto then have G:"converse(g)``(X-T)=X ⟶ g``(g-``(X-T))=g``(X-T)" by auto have GG:"g``(g-``(X-T))=(X-T)" using sub1 surj_image_vimage bij unfolding bij_def by auto with G have "converse(g)``(X-T)=X ⟶ g``(X-T)=X-T" by auto then have "converse(g)``(X-T)=X ⟶ g∈{f∈bij(X,X). f``(X-T)=(X-T)}" using bij by auto moreover from hom have "IsAhomeomorphism(ExcludedSet(X,T), ExcludedSet(X,T), converse(g))" using homeo_inv by auto moreover note hom ultimately have "g∈{f∈bij(X,X). f``(X-T)=(X-T)} ∨ (g``(X-T)⊆X-T ∧ converse(g)``(X-T)⊆X-T)" by force then have "g∈{f∈bij(X,X). f``(X-T)=(X-T)} ∨ (g``(X-T)⊆X-T ∧ g-``(X-T)⊆X-T)" unfolding vimage_def by auto moreover have "g-``(X-T)⊆X-T ⟶ g``(g-``(X-T))⊆g``(X-T)" using func1_1_L8 by auto with GG have "g-``(X-T)⊆X-T ⟶ (X-T)⊆g``(X-T)" by force ultimately have "g∈{f∈bij(X,X). f``(X-T)=(X-T)} ∨ (g``(X-T)⊆X-T ∧ (X-T)⊆g``(X-T))" by auto then have "g∈{f∈bij(X,X). f``(X-T)=(X-T)}" using bij by auto } then show "HomeoG(ExcludedSet(X,T))⊆{f∈bij(X,X). f``(X-T)=(X-T)}" by auto { fix g assume as:"g∈bij(X,X)""g``(X-T)=X-T" then have inj:"g∈inj(X,X)" and im:"g-``(g``(X-T))=g-``(X-T)" unfolding bij_def by auto from inj have "g-``(g``(X-T))=X-T" using inj_vimage_image sub1 by force with im have as_3:"g-``(X-T)=X-T" by auto { fix A assume "A∈(ExcludedSet(X,T))" then have "A=X∨A∩T=0" "A⊆X" unfolding ExcludedSet_def by auto then have "A⊆X-T∨A=X" by auto moreover { assume "A=X" with as(1) have "g``A=X" using surj_range_image_domain unfolding bij_def by auto } moreover { assume "A⊆X-T" then have "g``A⊆g``(X-T)" using func1_1_L8 by auto then have "g``A⊆(X-T)" using as(2) by auto } ultimately have "g``A⊆(X-T) ∨ g``A=X" by auto then have "g``A∈(ExcludedSet(X,T))" unfolding ExcludedSet_def by auto } then have "∀A∈(ExcludedSet(X,T)). g``A∈(ExcludedSet(X,T))" by auto moreover { fix A assume "A∈(ExcludedSet(X,T))" then have "A=X∨A∩T=0" "A⊆X" unfolding ExcludedSet_def by auto then have "A⊆X-T∨A=X" by auto moreover { assume "A=X" with as(1) have "g-``A=X" using func1_1_L4 unfolding bij_def inj_def by auto } moreover { assume "A⊆X-T" then have "g-``A⊆g-``(X-T)" using func1_1_L8 by auto then have "g-``A⊆(X-T)" using as_3 by auto } ultimately have "g-``A⊆(X-T) ∨ g-``A=X" by auto then have "g-``A∈(ExcludedSet(X,T))" unfolding ExcludedSet_def by auto } then have "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),g)" unfolding IsContinuous_def by auto moreover note as(1) ultimately have "IsAhomeomorphism(ExcludedSet(X,T),ExcludedSet(X,T),g)" using union_excludedset bij_cont_open_homeo by auto with as(1) have "g∈HomeoG(ExcludedSet(X,T))" unfolding bij_def inj_def HomeoG_def using union_excludedset by auto } then show "{f ∈ bij(X, X) . f `` (X - T) = X - T} ⊆ HomeoG(ExcludedSet(X,T))" by auto qed text‹We now give some lemmas that will help us compute ‹HomeoG(IncludedSet(X,T))›.› lemma cont_in_cont_ex: assumes "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),f)" "f:X→X" "T⊆X" shows "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),f)" proof- from assms(2,3) have two:"two_top_spaces0(IncludedSet(X,T),IncludedSet(X,T),f)" using union_includedset includedset_is_topology unfolding two_top_spaces0_def by auto { fix A assume "A∈(ExcludedSet(X,T))" then have "A∩T=0 ∨ A=X""A⊆X" unfolding ExcludedSet_def by auto then have "A{is closed in}(IncludedSet(X,T))" using closed_sets_includedset assms by auto then have "f-``A{is closed in}(IncludedSet(X,T))" using two_top_spaces0.TopZF_2_1_L1 assms(1) two assms includedset_is_topology by auto then have "(f-``A)∩T=0 ∨ f-``A=X""f-``A⊆X" using closed_sets_includedset assms(1,3) by auto then have "f-``A∈(ExcludedSet(X,T))" unfolding ExcludedSet_def by auto } then show "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),f)" unfolding IsContinuous_def by auto qed lemma cont_ex_cont_in: assumes "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),f)" "f:X→X" "T⊆X" shows "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),f)" proof- from assms(2) have two:"two_top_spaces0(ExcludedSet(X,T),ExcludedSet(X,T),f)" using union_excludedset excludedset_is_topology unfolding two_top_spaces0_def by auto { fix A assume "A∈(IncludedSet(X,T))" then have "T⊆A ∨ A=0""A⊆X" unfolding IncludedSet_def by auto then have "A{is closed in}(ExcludedSet(X,T))" using closed_sets_excludedset assms by auto then have "f-``A{is closed in}(ExcludedSet(X,T))" using two_top_spaces0.TopZF_2_1_L1 assms(1) two assms excludedset_is_topology by auto then have "T⊆(f-``A) ∨ f-``A=0""f-``A⊆X" using closed_sets_excludedset assms(1,3) by auto then have "f-``A∈(IncludedSet(X,T))" unfolding IncludedSet_def by auto } then show "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),f)" unfolding IsContinuous_def by auto qed text‹The previous lemmas imply that the group of homeomorphisms of the included set topology is the same as the one of the excluded set topology.› lemma homeo_included: assumes "T⊆X" shows "HomeoG(IncludedSet(X,T))={f ∈ bij(X, X) . f `` (X - T) = X - T}" proof- { fix f assume "f∈HomeoG(IncludedSet(X,T))" then have hom:"IsAhomeomorphism(IncludedSet(X,T),IncludedSet(X,T),f)" and fun:"f∈X→X" and bij:"f∈bij(X,X)" unfolding HomeoG_def IsAhomeomorphism_def using union_includedset assms by auto then have cont:"IsContinuous(IncludedSet(X,T),IncludedSet(X,T),f)" unfolding IsAhomeomorphism_def by auto then have "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),f)" using cont_in_cont_ex fun assms by auto moreover { from hom have cont1:"IsContinuous(IncludedSet(X,T),IncludedSet(X,T),converse(f))" unfolding IsAhomeomorphism_def by auto moreover have "converse(f):X→X" using bij_converse_bij bij unfolding bij_def inj_def by auto moreover note assms ultimately have "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),converse(f))" using cont_in_cont_ex assms by auto } then have "IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),converse(f))" by auto moreover note bij ultimately have "IsAhomeomorphism(ExcludedSet(X,T),ExcludedSet(X,T),f)" unfolding IsAhomeomorphism_def using union_excludedset by auto with fun have "f∈HomeoG(ExcludedSet(X,T))" unfolding HomeoG_def using union_excludedset by auto } then have "HomeoG(IncludedSet(X,T))⊆HomeoG(ExcludedSet(X,T))" by auto moreover { fix f assume "f∈HomeoG(ExcludedSet(X,T))" then have hom:"IsAhomeomorphism(ExcludedSet(X,T),ExcludedSet(X,T),f)" and fun:"f∈X→X" and bij:"f∈bij(X,X)" unfolding HomeoG_def IsAhomeomorphism_def using union_excludedset assms by auto then have cont:"IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),f)" unfolding IsAhomeomorphism_def by auto then have "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),f)" using cont_ex_cont_in fun assms by auto moreover { from hom have cont1:"IsContinuous(ExcludedSet(X,T),ExcludedSet(X,T),converse(f))" unfolding IsAhomeomorphism_def by auto moreover have "converse(f):X→X" using bij_converse_bij bij unfolding bij_def inj_def by auto moreover note assms ultimately have "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),converse(f))" using cont_ex_cont_in assms by auto } then have "IsContinuous(IncludedSet(X,T),IncludedSet(X,T),converse(f))" by auto moreover note bij ultimately have "IsAhomeomorphism(IncludedSet(X,T),IncludedSet(X,T),f)" unfolding IsAhomeomorphism_def using union_includedset assms by auto with fun have "f∈HomeoG(IncludedSet(X,T))" unfolding HomeoG_def using union_includedset assms by auto } then have "HomeoG(ExcludedSet(X,T))⊆HomeoG(IncludedSet(X,T))" by auto ultimately show ?thesis using homeo_excluded by auto qed text‹Finally, let's compute part of the group of homeomorphisms of an order topology.› lemma homeo_order: assumes "IsLinOrder(X,r)""∃x y. x≠y∧x∈X∧y∈X" shows "ord_iso(X,r,X,r)⊆HomeoG(OrdTopology X r)" proof fix f assume "f∈ord_iso(X,r,X,r)" then have bij:"f∈bij(X,X)" and ord:"∀x∈X. ∀y∈X. ⟨x, y⟩ ∈ r ⟷ ⟨f ` x, f ` y⟩ ∈ r" unfolding ord_iso_def by auto have twoSpac:"two_top_spaces0(OrdTopology X r,OrdTopology X r,f)" unfolding two_top_spaces0_def using bij unfolding bij_def inj_def using union_ordtopology[OF assms] Ordtopology_is_a_topology(1)[OF assms(1)] by auto { fix c d assume A:"c∈X""d∈X" { fix x assume AA:"x∈X""x≠c""x≠d""⟨c,x⟩∈r""⟨x,d⟩∈r" then have "⟨f`c,f`x⟩∈r""⟨f`x,f`d⟩∈r" using A(2,1) ord by auto moreover { assume "f`x=f`c ∨ f`x=f`d" then have "x=c∨x=d" using bij unfolding bij_def inj_def using A(2,1) AA(1) by auto then have "False" using AA(2,3) by auto } then have "f`x≠f`c""f`x≠f`d" by auto moreover have "f`x∈X" using bij unfolding bij_def inj_def using apply_type AA(1) by auto ultimately have "f`x∈IntervalX(X,r,f`c,f`d)" unfolding IntervalX_def Interval_def by auto } then have "{f`x. x∈IntervalX(X,r,c,d)}⊆IntervalX(X,r,f`c,f`d)" unfolding IntervalX_def Interval_def by auto moreover { fix y assume "y∈IntervalX(X,r,f`c,f`d)" then have y:"y∈X""y≠f`c""y≠f`d""⟨f`c,y⟩∈r""⟨y,f`d⟩∈r" unfolding IntervalX_def Interval_def by auto then obtain s where s:"s∈X""y=f`s" using bij unfolding bij_def surj_def by auto { assume "s=c∨s=d" then have "f`s=f`c∨f`s=f`d" by auto then have "False" using s(2) y(2,3) by auto } then have "s≠c""s≠d" by auto moreover have "⟨c,s⟩∈r""⟨s,d⟩∈r" using y(4,5) s ord A(2,1) by auto moreover note s(1) ultimately have "s∈IntervalX(X,r,c,d)" unfolding IntervalX_def Interval_def by auto then have "y∈{f`x. x∈IntervalX(X,r,c,d)}" using s(2) by auto } ultimately have "{f`x. x∈IntervalX(X,r,c,d)}=IntervalX(X,r,f`c,f`d)" by auto moreover have "IntervalX(X,r,c,d)⊆X" unfolding IntervalX_def by auto moreover have "f:X→X" using bij unfolding bij_def surj_def by auto ultimately have "f``IntervalX(X,r,c,d)=IntervalX(X,r,f`c,f`d)" using func_imagedef by auto } then have inter:"∀c∈X. ∀d∈X. f``IntervalX(X,r,c,d)=IntervalX(X,r,f`c,f`d) ∧ f`c∈X ∧ f`d∈X" using bij unfolding bij_def inj_def by auto { fix c assume A:"c∈X" { fix x assume AA:"x∈X""x≠c""⟨c,x⟩∈r" then have "⟨f`c,f`x⟩∈r" using A ord by auto moreover { assume "f`x=f`c" then have "x=c" using bij unfolding bij_def inj_def using A AA(1) by auto then have "False" using AA(2) by auto } then have "f`x≠f`c" by auto moreover have "f`x∈X" using bij unfolding bij_def inj_def using apply_type AA(1) by auto ultimately have "f`x∈RightRayX(X,r,f`c)" unfolding RightRayX_def by auto } then have "{f`x. x∈RightRayX(X,r,c)}⊆RightRayX(X,r,f`c)" unfolding RightRayX_def by auto moreover { fix y assume "y∈RightRayX(X,r,f`c)" then have y:"y∈X""y≠f`c""⟨f`c,y⟩∈r" unfolding RightRayX_def by auto then obtain s where s:"s∈X""y=f`s" using bij unfolding bij_def surj_def by auto { assume "s=c" then have "f`s=f`c" by auto then have "False" using s(2) y(2) by auto } then have "s≠c" by auto moreover have "⟨c,s⟩∈r" using y(3) s ord A by auto moreover note s(1) ultimately have "s∈RightRayX(X,r,c)" unfolding RightRayX_def by auto then have "y∈{f`x. x∈RightRayX(X,r,c)}" using s(2) by auto } ultimately have "{f`x. x∈RightRayX(X,r,c)}=RightRayX(X,r,f`c)" by auto moreover have "RightRayX(X,r,c)⊆X" unfolding RightRayX_def by auto moreover have "f:X→X" using bij unfolding bij_def surj_def by auto ultimately have "f``RightRayX(X,r,c)=RightRayX(X,r,f`c)" using func_imagedef by auto } then have rray:"∀c∈X. f``RightRayX(X,r,c)=RightRayX(X,r,f`c) ∧ f`c∈X" using bij unfolding bij_def inj_def by auto { fix c assume A:"c∈X" { fix x assume AA:"x∈X""x≠c""⟨x,c⟩∈r" then have "⟨f`x,f`c⟩∈r" using A ord by auto moreover { assume "f`x=f`c" then have "x=c" using bij unfolding bij_def inj_def using A AA(1) by auto then have "False" using AA(2) by auto } then have "f`x≠f`c" by auto moreover have "f`x∈X" using bij unfolding bij_def inj_def using apply_type AA(1) by auto ultimately have "f`x∈LeftRayX(X,r,f`c)" unfolding LeftRayX_def by auto } then have "{f`x. x∈LeftRayX(X,r,c)}⊆LeftRayX(X,r,f`c)" unfolding LeftRayX_def by auto moreover { fix y assume "y∈LeftRayX(X,r,f`c)" then have y:"y∈X""y≠f`c""⟨y,f`c⟩∈r" unfolding LeftRayX_def by auto then obtain s where s:"s∈X""y=f`s" using bij unfolding bij_def surj_def by auto { assume "s=c" then have "f`s=f`c" by auto then have "False" using s(2) y(2) by auto } then have "s≠c" by auto moreover have "⟨s,c⟩∈r" using y(3) s ord A by auto moreover note s(1) ultimately have "s∈LeftRayX(X,r,c)" unfolding LeftRayX_def by auto then have "y∈{f`x. x∈LeftRayX(X,r,c)}" using s(2) by auto } ultimately have "{f`x. x∈LeftRayX(X,r,c)}=LeftRayX(X,r,f`c)" by auto moreover have "LeftRayX(X,r,c)⊆X" unfolding LeftRayX_def by auto moreover have "f:X→X" using bij unfolding bij_def surj_def by auto ultimately have "f``LeftRayX(X,r,c)=LeftRayX(X,r,f`c)" using func_imagedef by auto } then have lray:"∀c∈X. f``LeftRayX(X,r,c)=LeftRayX(X,r,f`c)∧f`c∈X" using bij unfolding bij_def inj_def by auto have r1:"∀U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}. f``U∈({IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X})" apply safe prefer 3 using rray apply blast prefer 2 using lray apply blast using inter apply auto proof- fix xa y assume "xa∈X""y∈X" then have "f`xa∈X""f`y∈X" using bij unfolding bij_def inj_def by auto then show "∃x∈X. ∃ya∈X. IntervalX(X, r, f ` xa, f ` y) = IntervalX(X, r, x, ya)" by auto qed have r2:"{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}⊆(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by blast { fix U assume "U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}" with r1 have "f``U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}" by auto with r2 have "f``U∈(OrdTopology X r)" by blast } then have "∀U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}. f``U∈(OrdTopology X r)" by blast then have f_open:"∀U∈(OrdTopology X r). f``U∈(OrdTopology X r)" using two_top_spaces0.base_image_open[OF twoSpac Ordtopology_is_a_topology(2)[OF assms(1)]] by auto { fix c d assume A:"c∈X""d∈X" then obtain cc dd where pre:"f`cc=c""f`dd=d""cc∈X""dd∈X" using bij unfolding bij_def surj_def by blast with inter have "f `` IntervalX(X, r, cc, dd) = IntervalX(X, r, c, d)" by auto then have "f-``(f``IntervalX(X, r, cc, dd)) = f-``(IntervalX(X, r, c, d))" by auto moreover have "IntervalX(X, r, cc, dd)⊆X" unfolding IntervalX_def by auto moreover have "f∈inj(X,X)" using bij unfolding bij_def by auto ultimately have "IntervalX(X, r, cc, dd)=f-``IntervalX(X, r, c, d)" using inj_vimage_image by auto moreover from pre(3,4) have "IntervalX(X, r, cc, dd)∈{IntervalX(X,r,e1,e2). ⟨e1,e2⟩∈X×X}" by auto ultimately have "f-``IntervalX(X, r, c, d)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto } then have inter:"∀c∈X. ∀d∈X. f-``IntervalX(X, r, c, d)∈(OrdTopology X r)" by auto { fix c assume A:"c∈X" then obtain cc where pre:"f`cc=c""cc∈X" using bij unfolding bij_def surj_def by blast with rray have "f `` RightRayX(X, r, cc) = RightRayX(X, r, c)" by auto then have "f-``(f``RightRayX(X, r, cc)) = f-``(RightRayX(X, r, c))" by auto moreover have "RightRayX(X, r, cc)⊆X" unfolding RightRayX_def by auto moreover have "f∈inj(X,X)" using bij unfolding bij_def by auto ultimately have "RightRayX(X, r, cc)=f-``RightRayX(X, r, c)" using inj_vimage_image by auto moreover from pre(2) have "RightRayX(X, r, cc)∈{RightRayX(X,r,e2). e2∈X}" by auto ultimately have "f-``RightRayX(X, r, c)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto } then have rray:"∀c∈X. f-``RightRayX(X, r, c)∈(OrdTopology X r)" by auto { fix c assume A:"c∈X" then obtain cc where pre:"f`cc=c""cc∈X" using bij unfolding bij_def surj_def by blast with lray have "f `` LeftRayX(X, r, cc) = LeftRayX(X, r, c)" by auto then have "f-``(f``LeftRayX(X, r, cc)) = f-``(LeftRayX(X, r, c))" by auto moreover have "LeftRayX(X, r, cc)⊆X" unfolding LeftRayX_def by auto moreover have "f∈inj(X,X)" using bij unfolding bij_def by auto ultimately have "LeftRayX(X, r, cc)=f-``LeftRayX(X, r, c)" using inj_vimage_image by auto moreover from pre(2) have "LeftRayX(X, r, cc)∈{LeftRayX(X,r,e2). e2∈X}" by auto ultimately have "f-``LeftRayX(X, r, c)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto } then have lray:"∀c∈X. f-``LeftRayX(X, r, c)∈(OrdTopology X r)" by auto { fix U assume "U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}" with lray inter rray have "f-``U∈(OrdTopology X r)" by auto } then have "∀U∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}. f-``U∈(OrdTopology X r)" by blast then have fcont:"IsContinuous(OrdTopology X r,OrdTopology X r,f)" using two_top_spaces0.Top_ZF_2_1_L5[OF twoSpac Ordtopology_is_a_topology(2)[OF assms(1)]] by auto from fcont f_open bij have "IsAhomeomorphism(OrdTopology X r,OrdTopology X r,f)" using bij_cont_open_homeo union_ordtopology[OF assms] by auto then show "f∈HomeoG(OrdTopology X r)" unfolding HomeoG_def using bij union_ordtopology[OF assms] unfolding bij_def inj_def by auto qed text‹This last example shows that order isomorphic sets give homeomorphic topological spaces.› subsection‹Properties preserved by functions› text‹The continuous image of a connected space is connected.› theorem (in two_top_spaces0) cont_image_conn: assumes "IsContinuous(τ⇩_{1},τ⇩_{2},f)" "f∈surj(X⇩_{1},X⇩_{2})" "τ⇩_{1}{is connected}" shows "τ⇩_{2}{is connected}" proof- { fix U assume Uop:"U∈τ⇩_{2}" and Ucl:"U{is closed in}τ⇩_{2}" from Uop assms(1) have "f-``U∈τ⇩_{1}" unfolding IsContinuous_def by auto moreover from Ucl assms(1) have "f-``U{is closed in}τ⇩_{1}" using TopZF_2_1_L1 by auto ultimately have disj:"f-``U=0 ∨ f-``U=⋃τ⇩_{1}" using assms(3) unfolding IsConnected_def by auto moreover { assume as:"f-``U≠0" then have "U≠0" using func1_1_L13 by auto from as disj have "f-``U=⋃τ⇩_{1}" by auto then have "f``(f-``U)=f``(⋃τ⇩_{1})" by auto moreover have "U⊆⋃τ⇩_{2}" using Uop by blast ultimately have "U=f``(⋃τ⇩_{1})" using surj_image_vimage assms(2) Uop by force then have "⋃τ⇩_{2}=U" using surj_range_image_domain assms(2) by auto } moreover { assume as:"U≠0" from Uop have s:"U⊆⋃τ⇩_{2}" by auto with as obtain u where uU:"u∈U" by auto with s have "u∈⋃τ⇩_{2}" by auto with assms(2) obtain w where "f`w=u""w∈⋃τ⇩_{1}" unfolding surj_def X1_def X2_def by blast with uU have "w∈f-``U" using func1_1_L15 assms(2) unfolding surj_def by auto then have "f-``U≠0" by auto } ultimately have "U=0∨U=⋃τ⇩_{2}" by auto } then show ?thesis unfolding IsConnected_def by auto qed text‹Every continuous function from a space which has some property ‹P› and a space which has the property ‹anti(P)›, given that this property is preserved by continuous functions, if follows that the range of the function is in the spectrum. Applied to connectedness, it follows that continuous functions from a connected space to a totally-disconnected one are constant.› corollary(in two_top_spaces0) cont_conn_tot_disc: assumes "IsContinuous(τ⇩_{1},τ⇩_{2},f)" "τ⇩_{1}{is connected}" "τ⇩_{2}{is totally-disconnected}" "f:X⇩_{1}→X⇩_{2}" "X⇩_{1}≠0" shows "∃q∈X⇩_{2}. ∀w∈X⇩_{1}. f`(w)=q" proof- from assms(4) have surj:"f∈surj(X⇩_{1},range(f))" using fun_is_surj by auto have sub:"range(f)⊆X⇩_{2}" using func1_1_L5B assms(4) by auto from assms(1) have cont:"IsContinuous(τ⇩_{1},τ⇩_{2}{restricted to}range(f),f)" using restr_image_cont range_image_domain assms(4) by auto have union:"⋃(τ⇩_{2}{restricted to}range(f))=range(f)" unfolding RestrictedTo_def using sub by auto then have "two_top_spaces0(τ⇩_{1},τ⇩_{2}{restricted to}range(f),f)" unfolding two_top_spaces0_def using surj unfolding surj_def using tau1_is_top topology0.Top_1_L4 unfolding topology0_def using tau2_is_top by auto then have conn:"(τ⇩_{2}{restricted to}range(f)){is connected}" using two_top_spaces0.cont_image_conn surj assms(2) cont union by auto then have "range(f){is in the spectrum of}IsConnected" using assms(3) sub unfolding IsTotDis_def antiProperty_def using union by auto then have "range(f)≲1" using conn_spectrum by auto moreover from assms(5) have "f``X⇩_{1}≠0" using func1_1_L15A assms(4) by auto then have "range(f)≠0" using range_image_domain assms(4) by auto ultimately obtain q where uniq:"range(f)={q}" using lepoll_1_is_sing by blast { fix w assume "w∈X⇩_{1}" then have "f`w∈range(f)" using func1_1_L5A(2) assms(4) by auto with uniq have "f`w=q" by auto } then have "∀w∈X⇩_{1}. f`w=q" by auto then show ?thesis using uniq sub by auto qed text‹The continuous image of a compact space is compact.› theorem (in two_top_spaces0) cont_image_com: assumes "IsContinuous(τ⇩_{1},τ⇩_{2},f)" "f∈surj(X⇩_{1},X⇩_{2})" "X⇩_{1}{is compact of cardinal}K{in}τ⇩_{1}" shows "X⇩_{2}{is compact of cardinal}K{in}τ⇩_{2}" proof- have "X⇩_{2}⊆⋃τ⇩_{2}" by auto moreover { fix U assume as:"X⇩_{2}⊆⋃U" "U⊆τ⇩_{2}" then have P:"{f-``V. V∈U}⊆τ⇩_{1}" using assms(1) unfolding IsContinuous_def by auto from as(1) have "f-``X⇩_{2}⊆ f-``(⋃U)" by blast then have "f-``X⇩_{2}⊆ converse(f)``(⋃U)" unfolding vimage_def by auto moreover have "converse(f)``(⋃U)=(⋃V∈U. converse(f)``V)" using image_UN by force ultimately have "f-``X⇩_{2}⊆ (⋃V∈U. converse(f)``V)" by auto then have "f-``X⇩_{2}⊆ (⋃V∈U. f-``V)" unfolding vimage_def by auto then have "X⇩_{1}⊆ (⋃V∈U. f-``V)" using func1_1_L4 assms(2) unfolding surj_def by force then have "X⇩_{1}⊆ ⋃{f-``V. V∈U}" by auto with P assms(3) have "∃N∈Pow({f-``V. V∈U}). X⇩_{1}⊆ ⋃N ∧ N≺K" unfolding IsCompactOfCard_def by auto then obtain N where "N∈Pow({f-``V. V∈U})" "X⇩_{1}⊆ ⋃N" "N≺K" by auto then have fin:"N≺K" and sub:"N⊆{f-``V. V∈U}" and cov:"X⇩_{1}⊆ ⋃N" unfolding FinPow_def by auto from sub have "{f``R. R∈N}⊆{f``(f-``V). V∈U}" by auto moreover have "∀V∈U. V⊆⋃τ⇩_{2}" using as(2) by auto ultimately have "{f``R. R∈N}⊆U" using surj_image_vimage assms(2) by auto moreover let ?FN="{⟨R,f``R⟩. R∈N}" have FN:"?FN:N→{f``R. R∈N}" unfolding Pi_def function_def domain_def by auto { fix S assume "S∈{f``R. R∈N}" then obtain R where R_def:"R∈N""f``R=S" by auto then have "⟨R,f``R⟩∈?FN" by auto then have "?FN`R=f``R" using FN apply_equality by auto then have "∃R∈N. ?FN`R=S" using R_def by auto } then have surj:"?FN∈surj(N,{f``R. R∈N})" unfolding surj_def using FN by force from fin have N:"N≲K" "Ord(K)" using assms(3) lesspoll_imp_lepoll unfolding IsCompactOfCard_def using Card_is_Ord by auto then have "{f``R. R∈N}≲N" using surj_fun_inv_2 surj by auto then have "{f``R. R∈N}≺K" using fin lesspoll_trans1 by blast moreover have "⋃{f``R. R∈N}=f``(⋃N)" using image_UN by auto then have "f``X⇩_{1}⊆ ⋃{f``R. R∈N}" using cov by blast then have "X⇩_{2}⊆ ⋃{f``R. R∈N}" using assms(2) surj_range_image_domain by auto ultimately have "∃NN∈Pow(U). X⇩_{2}⊆ ⋃NN ∧ NN≺K" by auto } then have "∀U∈Pow(τ⇩_{2}). X⇩_{2}⊆ ⋃U ⟶ (∃NN∈Pow(U). X⇩_{2}⊆ ⋃NN ∧ NN≺K)" by auto ultimately show ?thesis using assms(3) unfolding IsCompactOfCard_def by auto qed text‹As it happends to connected spaces, a continuous function from a compact space to an anti-compact space has finite range.› corollary (in two_top_spaces0) cont_comp_anti_comp: assumes "IsContinuous(τ⇩_{1},τ⇩_{2},f)" "X⇩_{1}{is compact in}τ⇩_{1}" "τ⇩_{2}{is anti-compact}" "f:X⇩_{1}→X⇩_{2}" "X⇩_{1}≠0" shows "Finite(range(f))" and "range(f)≠0" proof- from assms(4) have surj:"f∈surj(X⇩_{1},range(f))" using fun_is_surj by auto have sub:"range(f)⊆X⇩_{2}" using func1_1_L5B assms(4) by auto from assms(1) have cont:"IsContinuous(τ⇩_{1},τ⇩_{2}{restricted to}range(f),f)" using restr_image_cont range_image_domain assms(4) by auto have union:"⋃(τ⇩_{2}{restricted to}range(f))=range(f)" unfolding RestrictedTo_def using sub by auto then have "two_top_spaces0(τ⇩_{1},τ⇩_{2}{restricted to}range(f),f)" unfolding two_top_spaces0_def using surj unfolding surj_def using tau1_is_top topology0.Top_1_L4 unfolding topology0_def using tau2_is_top by auto then have "range(f){is compact in}(τ⇩_{2}{restricted to}range(f))" using surj two_top_spaces0.cont_image_com cont union assms(2) Compact_is_card_nat by force then have "range(f){is in the spectrum of}(λT. (⋃T) {is compact in}T)" using assms(3) sub unfolding IsAntiComp_def antiProperty_def using union by auto then show "Finite(range(f))" using compact_spectrum by auto moreover from assms(5) have "f``X⇩_{1}≠0" using func1_1_L15A assms(4) by auto then show "range(f)≠0" using range_image_domain assms(4) by auto qed text‹As a consequence, it follows that quotient topological spaces of compact (connected) spaces are compact (connected).› corollary(in topology0) compQuot: assumes "(⋃T){is compact in}T" "equiv(⋃T,r)" shows "(⋃T)//r{is compact in}({quotient by}r)" proof- have surj:"{⟨b,r``{b}⟩. b∈⋃T}∈surj(⋃T,(⋃T)//r)" using quotient_proj_surj by auto moreover have tot:"⋃({quotient by}r)=(⋃T)//r" using total_quo_equi assms(2) by auto ultimately have cont:"IsContinuous(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont EquivQuo_def assms(2) by auto from surj tot have "two_top_spaces0(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" unfolding two_top_spaces0_def using topSpaceAssum equiv_quo_is_top assms(2) unfolding surj_def by auto with surj cont tot assms(1) show ?thesis using two_top_spaces0.cont_image_com Compact_is_card_nat by force qed corollary(in topology0) ConnQuot: assumes "T{is connected}" "equiv(⋃T,r)" shows "({quotient by}r){is connected}" proof- have surj:"{⟨b,r``{b}⟩. b∈⋃T}∈surj(⋃T,(⋃T)//r)" using quotient_proj_surj by auto moreover have tot:"⋃({quotient by}r)=(⋃T)//r" using total_quo_equi assms(2) by auto ultimately have cont:"IsContinuous(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont EquivQuo_def assms(2) by auto from surj tot have "two_top_spaces0(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" unfolding two_top_spaces0_def using topSpaceAssum equiv_quo_is_top assms(2) unfolding surj_def by auto with surj cont tot assms(1) show ?thesis using two_top_spaces0.cont_image_conn by force qed end