# Theory Topology_ZF_8

(*
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‹Suppose $T$ is a topology, $r$ is an equivalence relation on $X = \bigcup T$
and $P_r : X \rightarrow X/r$ maps an element of $X$ to its equivalence class
$r\{x \}$. Then we can define a topology (on $X/r$) by taking the collection of
those subsets $V$ of $X/r$ for which the inverse image by the projection $P_r$
is in $T$. This is the weakest topology on $X/r$ such that $P_r$ is continuous.
In this theory we consider a seemingly more general situation where we start with a topology
$T$ on $X=\bigcup T$ and a surjection $f:X\rightarrow Y$ and define
a topology on $Y$ by taking those subsets $V$ of $Y$ for which the inverse image
by the mapping $f$ is in $T$. Turns out that this construction is in a way equivalent
to the previous one as the topology defined this way is homeomorphic to
the topology defined by the equivalence relation $r_f$ on $X$ that relates
two elements of $X$ if $f$ has the same value on them. ›

subsection‹Definition of quotient topology›

text‹ In this section we define the quotient topology generated by a topology
$T$ and a surjection $f:\bigcup T \rightarrow Y$, and show its basic properties.  ›

text‹For a topological space $X=\bigcup T$ and a surjection $f:X\rightarrow Y$
we define ‹{quotient topology in} Y {by} f› as the collection of subsets
of $Y$ whose inverse images by $f$ are open. ›

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}"

text‹Outside of the ‹topology0› context we will indicate also the generating
topology and write ‹{quotient topology in} Y {by} f {from} X›. ›

abbreviation QuotientTopTop ("{quotient topology in}_{by}_{from}_")
where "{quotient topology in} Y {by} f {from} 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
moreover
{
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
}
hence "(⋃A∈M. f-(A)) = (⋃y∈⋃M. f-{y})" by auto
with A1 have A2: "f-(⋃M)=⋃{f- A. A∈M}" by auto
moreover
{
fix A assume "A∈M"
with M have "f-(A)∈T" by auto
}
hence "{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∩V)∈T" using topSpaceAssum invim_inter_inter_invim assms
unfolding IsATopology_def 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(τ⇩1,τ⇩2,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
with assms(1) have "g-(U)∈({quotient topology in} Y {by} h {from} τ⇩1)"
using topology0.QuotientTop_def tau1_is_top 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‹The quotient projection $b\mapsto r\{ b\}$ is a function that maps the domain of the
relation to the quotient. Note we do not need to assume that $r$ is an equivalence relation. ›

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

text‹The quotient projection is a surjection. Again $r$ does not need to be an equivalence relation
here ›

lemma quotient_proj_surj:
shows "{⟨b,r{b}⟩. b∈A}∈surj(A,A//r)"
proof-
{ fix y assume "y∈A//r"
then obtain x where "x∈A" "y=r{x}" unfolding quotient_def by auto
then have "∃x∈A. {⟨b,r{b}⟩. b∈A}(x) = y" using ZF_fun_from_tot_val1
by auto
}
then show ?thesis using quotient_proj_fun unfolding surj_def by auto
qed

text‹The inverse image of a subset $U$ of the quotient by the quotient projection is the union
of $U$. Note since $U$ is a subset of $A/r$ it is a collection of equivalence classes.›

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 "y∈V" and "V∈U" by auto
with assms have "y ∈ {⟨b,r{b}⟩. b∈A}-(U)"
using EquivClass_1_L1 EquivClass_1_L2 by blast
}
thus "⋃U⊆{⟨b,r{b}⟩. b∈A}-U" by blast
{
fix y assume "y∈{⟨b,r{b}⟩. b∈A}-U"
then have yy: "y∈{x∈A. r{x}∈U}" by auto
hence "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
}
thus "{⟨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}"

text‹Outside of the ‹topology0› context we need to indicate the original topology. ›

abbreviation EquivQuoTop ("_{quotient by}_")
where "T {quotient by} 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}"
with assms have "U∈{U∈Pow((⋃T)//r). ⋃U∈T}" using preim_equi_proj by auto
}
thus "{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}"
with assms have "U∈{U∈Pow((⋃T)//r). {⟨b,r{b}⟩. b∈⋃T}-U∈T}" using preim_equi_proj
by auto
}
thus "{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

text‹The quotient by an equivalence relation is indeed a topology. ›

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‹The next theorem is the main result of this section:
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-
from assms(1) have ff: "f:⋃T→Y" unfolding surj_def by auto
from assms(2) show B: "equiv(⋃T,r)"
unfolding equiv_def refl_def sym_def trans_def 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 assms(1) Y obtain A where A1: "A∈⋃T" "f(A)=y" unfolding surj_def
by blast
with ff have A: "A ∈ f-{y}" using func1_1_L15 by simp
{ fix t assume "t∈f-{y}"
with A eq have "t∈⋃T" "A∈⋃T" "⟨t,y⟩∈f" "⟨A,y⟩∈f" by auto
then have "ft=fA" using apply_equality assms(1) unfolding surj_def by auto
with assms(2) ‹t∈⋃T›‹A∈⋃T› have "⟨A,t⟩∈r" by auto
then have "t∈r{A}" using image_iff by auto
} hence "f-{y}⊆r{A}" by auto
moreover
{ fix t assume "t∈r{A}"
with assms(2) have un: "t∈⋃T" "A∈⋃T" and eq2: "f(t)=f(A)"
using image_iff by simp_all
from ff un have "⟨t,f(t)⟩∈f" using func1_1_L5A(1) by simp
with eq2 A1 un eq have "t∈f-{y}" by simp
} hence "r{A}⊆f-{y}" by auto
ultimately have "f-{y}=r{A}" by auto
with A1(1) have "f-{y} ∈ (⋃T)//r"
using A1(1) unfolding quotient_def by auto
with Y have "B∈Y×(⋃T)//r" by auto
} 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 P: "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. gy=f-{y}" using apply_equality gg by auto
ultimately have "f-s=(⋃y∈s. gy)" by auto
with P have "(⋃y∈s. gy)∈T" by auto
moreover from ‹s∈Pow(Y)› have "∀y∈s. gy∈(⋃T)//r" using apply_type gg by auto
ultimately have "{gy. y∈s}∈({quotient by}r)" using quotient_equiv_rel B by auto
with ‹s∈Pow(Y)› have "gs∈({quotient by}r)" using func_imagedef gg by auto
} hence gopen: "∀s∈({quotient topology in}Y{by}f). gs∈(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(fb)" using comp_fun_apply ff by auto
from bY have pg: "⟨fb,f-({fb})⟩∈g" unfolding g_def by auto
then have "g(fb) = f-({fb})" using apply_equality gg by auto
with com have comeq: "(g O f)b=f-({fb})" by auto
from b have A: "f{b}={fb}" "{b}⊆⋃T" using func_imagedef ff by auto
from A(2) have "b ∈ f-(f  {b})" using func1_1_L9 ff by blast
with A(1) have "b∈f-({fb})" by auto
moreover from pg have "f-({fb})∈(⋃T)//r" using gg unfolding Pi_def
by auto
ultimately have "r{b}=f-({fb})" using EquivClass_1_L2 B by auto
then have "(g O f)b=r{b}" using comeq by auto
moreover from b pr_fun have "{⟨b,r{b}⟩. b∈⋃T}b=r{b}"
using apply_equality by simp
ultimately  have "(g O f)b={⟨b,r{b}⟩. b∈⋃T}b" by simp
} hence reg: "∀b∈⋃T. (g O f)(b)={⟨b,r{b}⟩. b∈⋃T}(b)" by blast
moreover have compp: "g O f∈⋃T→(⋃T)//r" using comp_fun ff gg by blast
moreover
from compp pr_fun reg have feq: "(g O f)={⟨b,r{b}⟩. b∈⋃T}"
by (rule func_eq)
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 topSpaceAssum equiv_quo_is_top B
unfolding two_top_spaces0_def by auto
{ fix x y assume T: "x∈Y" "y∈Y" "g(x)=g(y)"
with assms(3) have "f(f-{x})=f(f-{y})"
using apply_equality gg by simp
with assms(1) T(1,2) have "x=y" using surj_image_vimage 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
with ff gg B have "g∈surj(Y,⋃(T{quotient by}r))"
using comp_mem_surjD1 total_quo_equi 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

text‹The mapping $\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$
is a function that maps the product of the carrier by itself to the
product of the quotients. Note $r$ does not have to be an equivalence relation. ›

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
hence "{⟨⟨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

text‹The mapping $\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$
is a surjection of the product of the carrier by itself onto the
carrier of the product topology. Again $r$ does not have to be an equivalence relation for this. ›

lemma (in topology0) prod_equiv_rel_surj:
shows "{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}∈surj(⋃(T×⇩tT),((⋃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
hence "⟨⟨m1,m2⟩,⟨r{m1},r{m2}⟩⟩∈{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}"
by auto
with fun have "{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}⟨m1,m2⟩=⟨r{m1},r{m2}⟩"
using apply_equality by auto
with M(1) m(3,4) mm have "∃R∈(⋃T×⋃T). {⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}(R) = M"
by auto
}
ultimately show ?thesis unfolding surj_def using Top_1_4_T1(3) topSpaceAssum
by auto
qed

text‹The product quotient projection (i.e. the mapping the mapping
$\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$ is continuous.›

lemma (in topology0) product_quo_fun:
assumes "equiv(⋃T,r)"
shows
"IsContinuous(T×⇩tT,({quotient by} r)×⇩t({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
hence 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
with assms have cont: "IsContinuous(T,{quotient by}r,{⟨b,r{b}⟩. b∈⋃T})"
using quotient_func_cont quotient_proj_surj EquivQuo_def by auto
with assms have  tot: "⋃(T{quotient by}r) = (⋃T) // r" and
top: "({quotient by}r) {is a topology}"
using total_quo_equi equiv_quo_is_top by auto
then have fun: "{⟨b,r{b}⟩. b∈⋃T}:⋃T→⋃({quotient by}r)" using quotient_proj_fun
by auto
then have "two_top_spaces0(T,{quotient by}r,{⟨b,r{b}⟩. b∈⋃T})"
unfolding two_top_spaces0_def using topSpaceAssum top by auto
with fun cont top IN show ?thesis
using two_top_spaces0.product_cont_functions topSpaceAssum 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 "(({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} (T×⇩tT))"
proof
let ?T⇩r = "{quotient by} r"
let ?R = "({quotient topology in} (((⋃T)//r)×((⋃T)//r)) {by} ({⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}) {from} (T×⇩tT))"
{ fix A assume A: "A∈?T⇩r×⇩t?T⇩r"
with assms(1) have "{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-(A) ∈ T×⇩tT"
using product_quo_fun unfolding IsContinuous_def by auto
moreover
from A have "A⊆⋃((?T⇩r)×⇩t(?T⇩r))" by auto
with assms(1) have "A∈Pow(((⋃T)//r)×((⋃T)//r))"
using Top_1_4_T1(3) equiv_quo_is_top total_quo_equi by auto
ultimately have "A∈?R"
using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj
unfolding topology0_def by auto
} thus "(?T⇩r)×⇩t(?T⇩r) ⊆ ?R" by auto
{ fix A assume "A∈?R"
with assms(1) have
A: "A ⊆ ((⋃T)//r)×((⋃T)//r)" "{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-(A) ∈ T×⇩tT"
using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj
unfolding topology0_def by auto
{ fix C assume "C∈A"
with A(1) obtain C⇩1 C⇩2 where CC: "C=⟨C⇩1,C⇩2⟩" "C⇩1∈((⋃T)//r)" "C⇩2∈((⋃T)//r)" by auto
then obtain c⇩1 c⇩2 where CC1: "c⇩1∈⋃T" "c⇩2∈⋃T" and CC2: "C⇩1=r{c⇩1}" "C⇩2=r{c⇩2}"
unfolding quotient_def by auto
with ‹C∈A› CC have "⟨c⇩1,c⇩2⟩∈{⟨⟨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) ∧ ⟨c⇩1,c⇩2⟩ ∈ 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)" "c⇩1∈V" "c⇩2∈W"
by blast
let ?V⇩r = "{⟨b,r{b}⟩. b∈⋃T}(V)"
let ?W⇩r = "{⟨b,r{b}⟩. b∈⋃T}(W)"
from VW assms have P: "(?V⇩r×?W⇩r) ∈ (?T⇩r)×⇩t(?T⇩r)"
using prod_open_open_prod equiv_quo_is_top by auto
{ fix S assume "S∈(?V⇩r×?W⇩r)"
then obtain s⇩1 s⇩2 where S: "S=⟨s⇩1,s⇩2⟩" "s⇩1∈?V⇩r" "s⇩2∈?W⇩r"
by blast
then obtain t⇩1 t⇩2 where
T: "⟨t⇩1,s⇩1⟩∈{⟨b,r{b}⟩. b∈⋃T}" "⟨t⇩2,s⇩2⟩∈{⟨b,r{b}⟩. b∈⋃T}" "t⇩1∈V" "t⇩2∈W"
using image_iff by auto
with VW(3) have "∃S⇩0∈A. ⟨⟨t⇩1,t⇩2⟩,S⇩0⟩∈{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}"
using vimage_iff by auto
then obtain S⇩0 where "S⇩0∈A" and
"⟨⟨t⇩1,t⇩2⟩,S⇩0⟩∈{⟨⟨b,c⟩,⟨r{b},r{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}"
by auto
moreover from S(1) T VW(1,2) have
"⟨⟨t⇩1,t⇩2⟩,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
} hence sub: "?V⇩r×?W⇩r ⊆ A" by blast
from CC CC2 CC1 ‹c⇩1∈V› ‹c⇩2∈W› have "C ∈ ?V⇩r×?W⇩r"
using image_iff by auto
with P sub have "∃U∈(?T⇩r)×⇩t(?T⇩r). U⊆A ∧ C∈U  "
by (rule witness_exists1)
} hence "∀C∈A. ∃U∈(?T⇩r)×⇩t(?T⇩r). C∈U ∧ U⊆A"
by blast
with assms(1) have "A∈(?T⇩r)×⇩t(?T⇩r)"
using topology0.open_neigh_open Top_1_4_T1 equiv_quo_is_top assms
unfolding topology0_def by auto
} thus "?R ⊆ (?T⇩r)×⇩t(?T⇩r)" by auto
qed

end
`