Theory Topology_ZF_8

theory Topology_ZF_8
imports Topology_ZF_6 EquivClass1
(* 
    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 8›

theory Topology_ZF_8 imports Topology_ZF_6 EquivClass1
begin

text{*This theory deals with quotient topologies.*}

subsection{*Definition of quotient topology*}

text{*Given a surjective function $f:X\to Y$ and a topology $\tau$ in $X$, it is
posible to consider a special topology in $Y$. $f$ is called quotient function.*}

definition(in topology0)
  QuotientTop ("{quotient topology in}_{by}_" 80)
  where "f∈surj(⋃T,Y) ⟹{quotient topology in}Y{by}f≡
    {U∈Pow(Y). f-``U∈T}"

abbreviation QuotientTopTop ("{quotient topology in}_{by}_{from}_")
  where "QuotientTopTop(Y,f,T) ≡ topology0.QuotientTop(T,Y,f)"

text{*The quotient topology is indeed a topology.*}

theorem(in topology0) quotientTop_is_top:
  assumes "f∈surj(⋃T,Y)"
  shows "({quotient topology in} Y {by} f) {is a topology}"
proof-
  have "({quotient topology in} Y {by} f)={U ∈ Pow(Y) . f -`` U ∈ T}" using QuotientTop_def assms
    by auto moreover
  {
    fix M x B assume M:"M ⊆ {U ∈ Pow(Y) . f -`` U ∈ T}"
    then have "⋃M⊆Y" by blast moreover
    have A1:"f -`` (⋃M)=(⋃y∈(⋃M). f-``{y})" using vimage_eq_UN by blast
    {
      fix A assume "A∈M"
      with M have "A∈Pow(Y)" "f -`` A∈T" by auto
      have "f -`` A=(⋃y∈A. f-``{y})" using vimage_eq_UN by blast
    }
    then have "(⋃A∈M. f-`` A)=(⋃A∈M. (⋃y∈A. f-``{y}))" by auto
    then have "(⋃A∈M. f-`` A)=(⋃y∈⋃M. f-``{y})" by auto
    with A1 have A2:"f -`` (⋃M)=⋃{f-`` A. A∈M}" by auto
    {
      fix A assume "A∈M"
      with M have "f -`` A∈T" by auto
    }
    then have "∀A∈M. f -`` A∈T" by auto
    then have "{f-`` A. A∈M}⊆T" by auto
    then have "(⋃{f-`` A. A∈M})∈T" using topSpaceAssum unfolding IsATopology_def by auto
    with A2 have "(f -`` (⋃M))∈T" by auto
    ultimately have "⋃M∈{U∈Pow(Y). f-``U∈T}" by auto
  }
  moreover
  {
    fix U V assume "U∈{U∈Pow(Y). f-``U∈T}""V∈{U∈Pow(Y). f-``U∈T}"
    then have "U∈Pow(Y)""V∈Pow(Y)""f-``U∈T""f-``V∈T" by auto
    then have "(f-``U)∩(f-``V)∈T" using topSpaceAssum unfolding IsATopology_def by auto
    then have "f-`` (U∩V)∈T" using invim_inter_inter_invim assms unfolding surj_def
      by auto
    with `U∈Pow(Y)``V∈Pow(Y)` have "U∩V∈{U∈Pow(Y). f-``U∈T}" by auto
  }
  ultimately show ?thesis using IsATopology_def by auto
qed

text{*The quotient function is continuous.*}

lemma (in topology0) quotient_func_cont:
  assumes "f∈surj(⋃T,Y)"
  shows "IsContinuous(T,({quotient topology in} Y {by} f),f)"
    unfolding IsContinuous_def using QuotientTop_def assms by auto

text{*One of the important properties of this topology, is that a function
from the quotient space is continuous iff the composition with the quotient
function is continuous.*}

theorem(in two_top_spaces0) cont_quotient_top:
  assumes "h∈surj(⋃τ1,Y)" "g:Y→⋃τ2" "IsContinuous(τ12,g O h)"
  shows "IsContinuous(({quotient topology in} Y {by} h {from} τ1),τ2,g)"
proof-
  {
    fix U assume "U∈τ2"
    with assms(3) have "(g O h)-``(U)∈τ1" unfolding IsContinuous_def by auto
    then have "h-``(g-``(U))∈τ1" using vimage_comp by auto
    then have "g-``(U)∈({quotient topology in} Y {by} h {from} τ1)" using topology0.QuotientTop_def
      tau1_is_top assms(1) using func1_1_L3 assms(2) unfolding topology0_def by auto
  }
  then show ?thesis unfolding IsContinuous_def by auto
qed

text{*The underlying set of the quotient topology is $Y$.*}

lemma(in topology0) total_quo_func:
  assumes "f∈surj(⋃T,Y)"
  shows "(⋃({quotient topology in}Y{by}f))=Y"
proof-
  from assms have "f-``Y=⋃T" using func1_1_L4 unfolding surj_def by auto moreover
  have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately
  have "Y∈({quotient topology in}Y{by}f{from}T)" using QuotientTop_def assms by auto
  then show ?thesis using QuotientTop_def assms by auto
qed

subsection{*Quotient topologies from equivalence relations*}
text{*In this section we will show that the quotient topologies come from
an equivalence relation.*}

text{*First, some lemmas for relations.*}

lemma quotient_proj_fun:
  shows "{⟨b,r``{b}⟩. b∈A}:A→A//r" unfolding Pi_def function_def domain_def
    unfolding quotient_def by auto

lemma quotient_proj_surj:
  shows "{⟨b,r``{b}⟩. b∈A}∈surj(A,A//r)"
proof-
  {
    fix y assume "y∈A//r"
    then obtain yy where A:"yy∈A" "y=r``{yy}" unfolding quotient_def by auto
    then have "⟨yy,y⟩∈{⟨b,r``{b}⟩. b∈A}" by auto
    then have "{⟨b,r``{b}⟩. b∈A}`yy=y" using apply_equality[OF _ quotient_proj_fun] by auto
    with A(1) have "∃yy∈A. {⟨b,r``{b}⟩. b∈A}`yy=y" by auto
  }
  with quotient_proj_fun show ?thesis unfolding surj_def by auto
qed 

lemma preim_equi_proj:
  assumes "U⊆A//r" "equiv(A,r)"
  shows "{⟨b,r``{b}⟩. b∈A}-``U=⋃U"
proof
  {
    fix y assume "y∈⋃U"
    then obtain V where V:"y∈V""V∈U" by auto
    with `U⊆(A//r)` have "y∈A" using EquivClass_1_L1 assms(2) by auto moreover
    from `U⊆(A//r)` V have "r``{y}=V" using EquivClass_1_L2 assms(2) by auto
    moreover note V(2) ultimately have "y∈{x∈A. r``{x}∈U}" by auto
    then have "y∈{⟨b,r``{b}⟩. b∈A}-``U" by auto
  }
  then show "⋃U⊆{⟨b,r``{b}⟩. b∈A}-``U" by blast moreover
  {
    fix y assume "y∈{⟨b,r``{b}⟩. b∈A}-``U"
    then have yy:"y∈{x∈A. r``{x}∈U}" by auto
    then have "r``{y}∈U" by auto moreover
    from yy have "y∈r``{y}" using assms equiv_class_self by auto ultimately
    have "y∈⋃U" by auto
  }
  then show "{⟨b,r``{b}⟩. b∈A}-``U⊆⋃U" by blast
qed

text{*Now we define what a quotient topology from an equivalence relation is:*}

definition(in topology0)
  EquivQuo ("{quotient by}_" 70)
  where "equiv(⋃T,r)⟹({quotient by}r)≡{quotient topology in}(⋃T)//r{by}{⟨b,r``{b}⟩. b∈⋃T}"

abbreviation
  EquivQuoTop ("_{quotient by}_" 60)
  where "EquivQuoTop(T,r)≡topology0.EquivQuo(T,r)"

text{*First, another description of the topology (more intuitive):*}

theorem (in topology0) quotient_equiv_rel:
  assumes "equiv(⋃T,r)"
  shows "({quotient by}r)={U∈Pow((⋃T)//r). ⋃U∈T}"
proof-
  have "({quotient topology in}(⋃T)//r{by}{⟨b,r``{b}⟩. b∈⋃T})={U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}"
    using QuotientTop_def quotient_proj_surj by auto moreover
  have "{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}={U∈Pow((⋃T)//r). ⋃U∈T}"
    proof
     {
       fix U assume "U∈{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}"
       then have "U∈{U∈Pow((⋃T)//r). ⋃U∈T}" using preim_equi_proj assms by auto
     }
     then show "{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}⊆{U∈Pow((⋃T)//r). ⋃U∈T}" by auto
     {
       fix U assume "U∈{U∈Pow((⋃T)//r). ⋃U∈T}"
       then have "U∈{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" using preim_equi_proj assms by auto
     }
     then show "{U∈Pow((⋃T)//r). ⋃U∈T}⊆{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" by auto
   qed
  ultimately show ?thesis using EquivQuo_def assms by auto
qed

text{*We apply previous results to this topology.*}

theorem(in topology0) total_quo_equi:
  assumes "equiv(⋃T,r)"
  shows "⋃({quotient by}r)=(⋃T)//r"
  using total_quo_func quotient_proj_surj EquivQuo_def assms by auto

theorem(in topology0) equiv_quo_is_top:
  assumes "equiv(⋃T,r)"
  shows "({quotient by}r){is a topology}"
  using quotientTop_is_top quotient_proj_surj EquivQuo_def assms by auto

text{*MAIN RESULT: All quotient topologies arise from an equivalence relation given by the quotient 
function $f:X\to Y$. This means that any quotient topology is homeomorphic to a topology
given by an equivalence relation quotient.*}

theorem(in topology0) equiv_quotient_top:
  assumes "f∈surj(⋃T,Y)"
  defines "r≡{⟨x,y⟩∈⋃T×⋃T. f`(x)=f`(y)}"
  defines "g≡{⟨y,f-``{y}⟩. y∈Y}"
  shows "equiv(⋃T,r)" and "IsAhomeomorphism(({quotient topology in}Y{by}f),({quotient by}r),g)"
proof-
  have ff:"f:⋃T→Y" using assms(1) unfolding surj_def by auto
  show B:"equiv(⋃T,r)" unfolding equiv_def refl_def sym_def trans_def unfolding r_def by auto
  have gg:"g:Y→((⋃T)//r)"
    proof-
      {
        fix B assume "B∈g"
        then obtain y where Y:"y∈Y" "B=⟨y,f-``{y}⟩" unfolding g_def by auto
        then have "f-``{y}⊆⋃T" using func1_1_L3 ff by blast
        then have eq:"f-``{y}={x∈⋃T. ⟨x,y⟩∈f}" using vimage_iff by auto
        from Y obtain A where A1:"A∈⋃T""f`A=y" using assms(1) unfolding surj_def by blast
        with eq have A:"A∈f-``{y}" using apply_Pair[OF ff] by auto
        {
          fix t assume "t∈f-``{y}"
          with A have "t∈⋃T""A∈⋃T""⟨t,y⟩∈f""⟨A,y⟩∈f" using eq by auto
          then have "f`t=f`A" using apply_equality assms(1) unfolding surj_def by auto
          with `t∈⋃T``A∈⋃T` have "⟨A,t⟩∈r" using r_def by auto
          then have "t∈r``{A}" using image_iff by auto
        }
        then have "f-``{y}⊆r``{A}" by auto moreover
        {
          fix t assume "t∈r``{A}"
          then have "⟨A,t⟩∈r" using image_iff by auto
          then have un:"t∈⋃T""A∈⋃T" and eq2:"f`t=f`A" unfolding r_def by auto moreover
          from un have "⟨t,f`t⟩∈f" using apply_Pair[OF ff] by auto
          with eq2 A1 have "⟨t,y⟩∈f" by auto
          with un have "t∈f-``{y}" using eq by auto
        }
        then have "r``{A}⊆f-``{y}" by auto ultimately
        have "f-``{y}=r``{A}" by auto
        then have "f-``{y}∈ (⋃T)//r" using A1(1) unfolding quotient_def by auto
        with Y have "B∈Y×(⋃T)//r" by auto
      }
      then have "∀A∈g. A∈ Y×(⋃T)//r" by auto
      then have "g⊆(Y×(⋃T)//r)" by auto moreover
      then show ?thesis unfolding Pi_def function_def domain_def g_def by auto
    qed
  then have gg2:"g:Y→(⋃({quotient by}r))" using total_quo_equi B by auto
  {
    fix s assume S:"s∈({quotient topology in}Y{by}f)"
    then have "s∈Pow(Y)"and op:"f-``s∈T" using QuotientTop_def topSpaceAssum assms(1)
      by auto
    have "f-``s=(⋃y∈s. f-``{y})" using vimage_eq_UN by blast moreover
    from `s∈Pow(Y)` have "∀y∈s. ⟨y,f-``{y}⟩∈g" unfolding g_def by auto
    then have "∀y∈s. g`y=f-``{y}" using apply_equality gg by auto ultimately
    have "f-``s=(⋃y∈s. g`y)" by auto
    with op have "(⋃y∈s. g`y)∈T" by auto moreover
    from `s∈Pow(Y)` have "∀y∈s. g`y∈(⋃T)//r" using apply_type gg by auto
    ultimately have "{g`y. y∈s}∈({quotient by}r)" using quotient_equiv_rel B by auto
    with `s∈Pow(Y)` have "g``s∈({quotient by}r)" using func_imagedef gg by auto
  }
  then have gopen:"∀s∈({quotient topology in}Y{by}f). g``s∈(T{quotient by}r)" by auto
  have pr_fun:"{⟨b,r``{b}⟩. b∈⋃T}:⋃T→(⋃T)//r" using quotient_proj_fun by auto
  {
    fix b assume b:"b∈⋃T"
    have bY:"f`b∈Y" using apply_funtype ff b by auto
    with b have com:"(g O f)`b=g`(f`b)" using comp_fun_apply ff by auto
    from bY have pg:"⟨f`b,f-``({f`b})⟩∈g" unfolding g_def by auto
    then have "g`(f`b)=f-``({f`b})" using apply_equality gg by auto
    with com have comeq:"(g O f)`b=f-``({f`b})" by auto
    from b have A:"f``{b}={f`b}" "{b}⊆⋃T" using func_imagedef ff by auto
    from A(2) have "b∈f -`` (f `` {b})" using func1_1_L9 ff by blast
    then have "b∈f-``({f`b})" using A(1) by auto moreover
    from pg have "f-``({f`b})∈(⋃T)//r" using gg unfolding Pi_def by auto
    ultimately have "r``{b}=f-``({f`b})" using EquivClass_1_L2 B by auto
    then have "(g O f)`b=r``{b}" using comeq by auto moreover
    from b have "⟨b,r``{b}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto
    with pr_fun have "{⟨b,r``{b}⟩. b∈⋃T}`b=r``{b}" using apply_equality by auto ultimately
    have "(g O f)`b={⟨b,r``{b}⟩. b∈⋃T}`b" by auto
  } 
  then have reg:"∀b∈⋃T. (g O f)`b={⟨b,r``{b}⟩. b∈⋃T}`b" by auto moreover
  have compp:"g O f∈⋃T→(⋃T)//r" using comp_fun ff gg by auto
  have feq:"(g O f)={⟨b,r``{b}⟩. b∈⋃T}" using fun_extension[OF compp pr_fun] reg by auto
  then have "IsContinuous(T,{quotient by}r,(g O f))" using quotient_func_cont quotient_proj_surj
    EquivQuo_def topSpaceAssum B by auto moreover
  have "(g O f):⋃T→⋃({quotient by}r)" using comp_fun ff gg2 by auto
  ultimately have gcont:"IsContinuous({quotient topology in}Y{by}f,{quotient by}r,g)"
    using two_top_spaces0.cont_quotient_top assms(1) gg2 unfolding two_top_spaces0_def
    using topSpaceAssum equiv_quo_is_top B by auto
  {
    fix x y assume T:"x∈Y""y∈Y""g`x=g`y"
      then have "f-``{x}=f-``{y}" using apply_equality gg unfolding g_def by auto
      then have "f``(f-``{x})=f``(f-``{y})" by auto
      with T(1,2) have "{x}={y}" using surj_image_vimage assms(1) by auto
      then have "x=y" by auto
  }
  with gg2 have "g∈inj(Y,⋃({quotient by}r))" unfolding inj_def by auto moreover
  have "g O f∈surj(⋃T, (⋃T)//r)" using feq quotient_proj_surj by auto
  then have "g∈surj(Y,(⋃T)//r)" using comp_mem_surjD1 ff gg by auto
  then have "g∈surj(Y,⋃(T{quotient by}r))" using total_quo_equi B by auto
  ultimately have "g∈bij(⋃({quotient topology in}Y{by}f),⋃({quotient by}r))" unfolding bij_def using total_quo_func assms(1) by auto
  with gcont gopen show "IsAhomeomorphism(({quotient topology in}Y{by}f),({quotient by}r),g)"
    using bij_cont_open_homeo by auto
qed

lemma product_equiv_rel_fun:
  shows "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:(⋃T×⋃T)→((⋃T)//r×(⋃T)//r)"
proof-
  have " {⟨b,r``{b}⟩. b∈⋃T}∈⋃T→(⋃T)//r" using quotient_proj_fun by auto moreover
  have "∀A∈⋃T. ⟨A,r``{A}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto
  ultimately have "∀A∈⋃T. {⟨b,r``{b}⟩. b∈⋃T}`A=r``{A}" using apply_equality by auto
  then have IN:" {⟨⟨b, c⟩, r `` {b}, r `` {c}⟩ . ⟨b,c⟩ ∈ ⋃T × ⋃T}= {⟨⟨x, y⟩, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` x, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` y⟩ . ⟨x,y⟩ ∈ ⋃T × ⋃T}"
    by force
  then show ?thesis using prod_fun quotient_proj_fun by auto
qed

lemma(in topology0) prod_equiv_rel_surj:
  shows "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:surj(⋃(ProductTopology(T,T)),((⋃T)//r×(⋃T)//r))"
proof-
  have fun:"{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:(⋃T×⋃T)→((⋃T)//r×(⋃T)//r)" using
    product_equiv_rel_fun by auto moreover
  {
    fix M assume "M∈((⋃T)//r×(⋃T)//r)"
    then obtain M1 M2 where M:"M=⟨M1,M2⟩" "M1∈(⋃T)//r""M2∈(⋃T)//r" by auto
    then obtain m1 m2 where m:"m1∈⋃T""m2∈⋃T""M1=r``{m1}""M2=r``{m2}" unfolding quotient_def
      by auto
    then have mm:"⟨m1,m2⟩∈(⋃T×⋃T)" by auto
    then have "⟨⟨m1,m2⟩,⟨r``{m1},r``{m2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto
    then have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`⟨m1,m2⟩=⟨r``{m1},r``{m2}⟩"
      using apply_equality fun by auto
    then have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`⟨m1,m2⟩=M" using M(1) m(3,4) by auto
    then have "∃R∈(⋃T×⋃T). {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`R=M" using mm by auto
  }
  ultimately show ?thesis unfolding surj_def using Top_1_4_T1(3) topSpaceAssum by auto
qed

lemma(in topology0) product_quo_fun:
  assumes "equiv(⋃T,r)"
  shows "IsContinuous(ProductTopology(T,T),ProductTopology({quotient by}r,({quotient by}r)),{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})"
proof-
  have "{⟨b,r``{b}⟩. b∈⋃T}:⋃T→(⋃T)//r" using quotient_proj_fun by auto moreover
  have "∀A∈⋃T. ⟨A,r``{A}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto ultimately
  have "∀A∈⋃T. {⟨b,r``{b}⟩. b∈⋃T}`A=r``{A}" using apply_equality by auto
  then have IN:" {⟨⟨b, c⟩, r `` {b}, r `` {c}⟩ . ⟨b,c⟩ ∈ ⋃T × ⋃T}= {⟨⟨x, y⟩, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` x, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` y⟩ . ⟨x,y⟩ ∈ ⋃T × ⋃T}"
    by force
  have cont:"IsContinuous(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont quotient_proj_surj
    EquivQuo_def assms by auto
  have tot:"⋃(T{quotient by}r) = (⋃T) // r" and top:"({quotient by}r) {is a topology}" using total_quo_equi equiv_quo_is_top assms by auto 
  then have fun:"{⟨b,r``{b}⟩. b∈⋃T}:⋃T→⋃({quotient by}r)" using quotient_proj_fun by auto
  then have two:"two_top_spaces0(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" unfolding two_top_spaces0_def using topSpaceAssum top by auto
  show ?thesis using two_top_spaces0.product_cont_functions two fun fun cont cont top topSpaceAssum IN by auto
qed

text{*The product of quotient topologies is a quotient topology given that the
quotient map is open. This isn't true in general.*}

theorem(in topology0) prod_quotient:
  assumes "equiv(⋃T,r)" "∀A∈T. {⟨b,r``{b}⟩. b∈⋃T}``A∈({quotient by}r)"
  shows "(ProductTopology({quotient by}r,{quotient by}r)) = ({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}({⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}){from}(ProductTopology(T,T)))"
proof
  {
    fix A assume A:"A∈ProductTopology({quotient by}r,{quotient by}r)"
    from assms have "IsContinuous(ProductTopology(T,T),ProductTopology({quotient by}r,({quotient by}r)),{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})" using product_quo_fun
      by auto
    with A have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A∈ProductTopology(T,T)"
      unfolding IsContinuous_def by auto moreover
    from A have "A⊆⋃ProductTopology(T{quotient by}r,T{quotient by}r)" by auto
    then have "A⊆⋃(T{quotient by}r)×⋃(T{quotient by}r)" using Top_1_4_T1(3) equiv_quo_is_top equiv_quo_is_top
      using assms by auto
    then have "A∈Pow(((⋃T)//r)×((⋃T)//r))" using total_quo_equi assms by auto
    ultimately have "A∈({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))"
      using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj assms(1) unfolding topology0_def by auto
  }
  then show "ProductTopology(T{quotient by}r,T{quotient by}r)⊆({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))"
    by auto
  {
    fix A assume "A∈({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))"
    then have A:"A⊆((⋃T)//r)×((⋃T)//r)" "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A∈ProductTopology(T,T)"
      using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj assms(1) unfolding topology0_def by auto
    {
      fix CC assume "CC∈A"
      with A(1) obtain C1 C2 where CC:"CC=⟨C1,C2⟩" "C1∈((⋃T)//r)""C2∈((⋃T)//r)" by auto
      then obtain c1 c2 where CC1:"c1∈⋃T""c2∈⋃T" and CC2:"C1=r``{c1}""C2=r``{c2}" unfolding quotient_def
        by auto
      then have "⟨c1,c2⟩∈⋃T×⋃T" by auto
      then have "⟨⟨c1,c2⟩,⟨r``{c1},r``{c2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto
      with CC2 CC have "⟨⟨c1,c2⟩,CC⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto
      with `CC∈A` have "⟨c1,c2⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A"
        using vimage_iff by auto
      with A(2) have " ∃V W. V ∈ T ∧ W ∈ T ∧ V × W ⊆ {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A ∧ ⟨c1,c2⟩ ∈ V × W"
         using prod_top_point_neighb topSpaceAssum by blast
      then obtain V W where VW:"V∈T""W∈T""V × W ⊆ {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A""c1∈V""c2∈W" by auto
      with assms(2) have "{⟨b,r``{b}⟩. b∈⋃T}``V∈(T{quotient by}r)""{⟨b,r``{b}⟩. b∈⋃T}``W∈(T{quotient by}r)" by auto
      then have op:"{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W∈ProductTopology(T{quotient by}r,T{quotient by}r)" using prod_open_open_prod equiv_quo_is_top
        assms(1) by auto
      {
        fix S assume "S∈{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W"
        then obtain s1 s2 where S:"S=⟨s1,s2⟩""s1∈{⟨b,r``{b}⟩. b∈⋃T}``V""s2∈{⟨b,r``{b}⟩. b∈⋃T}``W" by blast
        then obtain t1 t2 where T:"⟨t1,s1⟩∈{⟨b,r``{b}⟩. b∈⋃T}""⟨t2,s2⟩∈{⟨b,r``{b}⟩. b∈⋃T}""t1∈V""t2∈W" using image_iff by auto
        then have "⟨t1,t2⟩∈V×W" by auto
        with VW(3) have "⟨t1,t2⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A" by auto
        then have "∃SS∈A. ⟨⟨t1,t2⟩,SS⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" using vimage_iff by auto
        then obtain SS where "SS∈A""⟨⟨t1,t2⟩,SS⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto moreover       
        from T VW(1,2) have "⟨t1,t2⟩∈⋃T×⋃T""⟨s1,s2⟩=⟨r``{t1},r``{t2}⟩" by auto
        with S(1) have "⟨⟨t1,t2⟩,S⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto
        ultimately have "S∈A" using product_equiv_rel_fun unfolding Pi_def function_def
          by auto
      }
      then have sub:"{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W⊆A" by blast
      have "⟨c1,C1⟩∈{⟨b,r``{b}⟩. b∈⋃T}""⟨c2,C2⟩∈{⟨b,r``{b}⟩. b∈⋃T}" using CC2 CC1
        by auto
      with `c1∈V``c2∈W` have "C1∈{⟨b,r``{b}⟩. b∈⋃T}``V""C2∈{⟨b,r``{b}⟩. b∈⋃T}``W"
        using image_iff by auto
      then have "CC∈{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W" using CC by auto
      with sub op have "∃OO∈ProductTopology(T{quotient by}r,T{quotient by}r). CC∈OO∧ OO⊆A"
        using exI[where x="{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W" and P="λOO. OO∈ProductTopology(T{quotient by}r,T{quotient by}r)∧ CC∈OO∧ OO⊆A"]
        by auto
    }
    then have "∀C∈A. ∃OO∈ProductTopology(T{quotient by}r,T{quotient by}r). C∈OO∧ OO⊆A" by auto
    then have "A∈ProductTopology(T{quotient by}r,T{quotient by}r)" using topology0.open_neigh_open
      unfolding topology0_def using Top_1_4_T1 equiv_quo_is_top assms by auto
  }
  then show "({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))⊆ProductTopology(T{quotient by}r,T{quotient by}r)"
    by auto
qed

end