Theory Topology_ZF_9

(* 
    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