# Theory Topology_ZF_2

(*
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005 - 2022  Slawomir Kolodynski

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 2›

theory Topology_ZF_2 imports Topology_ZF_1 func1 Fol1

begin

text‹This theory continues the series on general topology and covers the
definition and basic properties of continuous functions. We also introduce the notion of
homeomorphism an prove the pasting lemma.›

subsection‹Continuous functions.›

text‹In this section we define continuous functions and prove that certain
conditions are equivalent to a function being continuous.›

text‹In standard math we say that a function is continuous with respect to two
topologies $\tau_1 ,\tau_2$ if the inverse image of sets from topology
$\tau_2$ are in $\tau_1$. Here we define a predicate that is supposed
to reflect that definition, with a difference that we don't require in the
definition that $\tau_1 ,\tau_2$ are topologies. This means for example that
when we define measurable functions, the definition will be the same.

The notation ‹f-(A)› means the inverse image of (a set)
$A$ with respect to (a function) $f$.
›

definition
"IsContinuous(τ⇩1,τ⇩2,f) ≡ (∀U∈τ⇩2. f-(U) ∈ τ⇩1)"

text‹The space of continuous functions mapping $X=\bigcup \tau_1$ to $Y=\bigcup \tau_2$
will be denoted ‹Cont(τ⇩1,τ⇩2)›. ›

definition
"Cont(τ⇩1,τ⇩2) ≡ {f∈(⋃τ⇩1)→(⋃τ⇩2). IsContinuous(τ⇩1,τ⇩2,f)}"

text‹A trivial example of a continuous function - identity is continuous.›

lemma id_cont: shows "IsContinuous(τ,τ,id(⋃τ))"
proof -
{ fix U assume "U∈τ"
then have "id(⋃τ)-(U) = U" using vimage_id_same by auto
with ‹U∈τ› have "id(⋃τ)-(U) ∈ τ" by simp
} then show "IsContinuous(τ,τ,id(⋃τ))" unfolding IsContinuous_def
by simp
qed

text‹Identity is in the space of continuous functions from $\bigcup \tau$ to itself.›

lemma id_cont_sp: shows "{⟨x,x⟩. x∈⋃τ} ∈ Cont(τ,τ)"
proof -
have "id(⋃τ) : ⋃τ → ⋃τ" and "IsContinuous(τ,τ,id(⋃τ))"
using id_type id_cont by auto
moreover have "id(⋃τ) = {⟨x,x⟩. x∈⋃τ}" by blast
ultimately show ?thesis unfolding Cont_def by simp
qed

text‹A constant function is continuous.›

lemma const_cont: assumes "T {is a topology}"
shows "IsContinuous(T,τ,ConstantFunction(⋃T,c))"
proof -
let ?C = "ConstantFunction(⋃T,c)"
{ fix U assume "U∈τ"
have "?C-(U) ∈ T"
proof -
{ assume "c∈U"
with assms have "?C-(U) ∈ T"  using carr_open const_vimage_domain
by simp
}
moreover
{ assume "c∉U"
with assms have "?C-(U) ∈ T" using empty_open const_vimage_empty
by simp
}
ultimately show "?C-(U) ∈ T" by auto
qed
} then show ?thesis unfolding IsContinuous_def
by simp
qed

text‹If $c\in Y = \bigcup S$, then the constant function defined on $X=\bigcup T$
that is equal to $c$ is in the the space of continuous functions from $X$ to $Y$.  ›

lemma const_cont_sp: assumes "T {is a topology}" "c∈⋃S"
shows "{⟨x,c⟩. x∈⋃T} ∈ Cont(T,S)"
using assms ZF_fun_from_total const_fun_def_alt const_cont
unfolding Cont_def by simp

text‹We will work with a pair of topological spaces. The following
locale sets up our context that consists of
two topologies $\tau_1,\tau_2$ and
a continuous function $f: X_1 \rightarrow X_2$, where $X_i$ is defined
as $\bigcup\tau_i$ for $i=1,2$. We also define notation ‹cl⇩1(A)› and
‹cl⇩2(A)› for closure of a set $A$ in topologies $\tau_1$ and $\tau_2$,
respectively.›

locale two_top_spaces0 =

fixes τ⇩1
assumes tau1_is_top: "τ⇩1 {is a topology}"

fixes τ⇩2
assumes tau2_is_top: "τ⇩2 {is a topology}"

fixes X⇩1
defines X1_def [simp]: "X⇩1 ≡ ⋃τ⇩1"

fixes X⇩2
defines X2_def [simp]: "X⇩2 ≡ ⋃τ⇩2"

fixes f
assumes fmapAssum: "f: X⇩1 → X⇩2"

fixes isContinuous ("_ {is continuous}" [50] 50)
defines isContinuous_def [simp]: "g {is continuous} ≡ IsContinuous(τ⇩1,τ⇩2,g)"

fixes cl⇩1
defines cl1_def [simp]: "cl⇩1(A) ≡ Closure(A,τ⇩1)"

fixes cl⇩2
defines cl2_def [simp]: "cl⇩2(A) ≡ Closure(A,τ⇩2)"

text‹First we show that theorems proven in locale ‹topology0›
are valid when applied to topologies $\tau_1$ and $\tau_2$.›

lemma (in two_top_spaces0) topol_cntxs_valid:
shows "topology0(τ⇩1)" and "topology0(τ⇩2)"
using tau1_is_top tau2_is_top topology0_def by auto

text‹For continuous functions the inverse image of a closed set is closed.›

lemma (in two_top_spaces0) TopZF_2_1_L1:
assumes A1: "f {is continuous}" and A2: "D {is closed in} τ⇩2"
shows "f-(D) {is closed in} τ⇩1"
proof -
from fmapAssum have  "f-(D) ⊆ X⇩1" using func1_1_L3 by simp
moreover from fmapAssum have "f-(X⇩2 - D) =  X⇩1 - f-(D)"
using Pi_iff function_vimage_Diff func1_1_L4 by auto
ultimately have "X⇩1 - f-(X⇩2 - D) = f-(D)" by auto
moreover from A1 A2 have "(X⇩1 - f-(X⇩2 - D)) {is closed in} τ⇩1"
using IsClosed_def IsContinuous_def topol_cntxs_valid topology0.Top_3_L9
by simp
ultimately show "f-(D) {is closed in} τ⇩1" by simp
qed

text‹If the inverse image of every closed set is closed, then the
image of a closure is contained in the closure of the image.›

lemma (in two_top_spaces0) Top_ZF_2_1_L2:
assumes A1: "∀D. ((D {is closed in} τ⇩2) ⟶ f-(D) {is closed in} τ⇩1)"
and A2: "A ⊆ X⇩1"
shows "f(cl⇩1(A)) ⊆ cl⇩2(f(A))"
proof -
from fmapAssum have "f(A) ⊆ cl⇩2(f(A))"
using func1_1_L6 topol_cntxs_valid topology0.cl_contains_set
by simp
with fmapAssum have "f-(f(A)) ⊆ f-(cl⇩2(f(A)))"
by auto
moreover from fmapAssum A2 have "A ⊆ f-(f(A))"
using func1_1_L9 by simp
ultimately have "A ⊆ f-(cl⇩2(f(A)))" by auto
with fmapAssum A1 have "f(cl⇩1(A)) ⊆ f(f-(cl⇩2(f(A))))"
using func1_1_L6 func1_1_L8 IsClosed_def
topol_cntxs_valid topology0.cl_is_closed topology0.Top_3_L13
by simp
moreover from fmapAssum have "f(f-(cl⇩2(f(A)))) ⊆ cl⇩2(f(A))"
using fun_is_function function_image_vimage by simp
ultimately show "f(cl⇩1(A)) ⊆ cl⇩2(f(A))"
by auto
qed

text‹If $f\left( \overline{A}\right)\subseteq \overline{f(A)}$
(the image of the closure is contained in the closure of the image), then
$\overline{f^{-1}(B)}\subseteq f^{-1}\left( \overline{B} \right)$
(the inverse image of the closure contains the closure of the
inverse image).›

lemma (in two_top_spaces0) Top_ZF_2_1_L3:
assumes A1: "∀ A. ( A ⊆ X⇩1 ⟶ f(cl⇩1(A)) ⊆ cl⇩2(f(A)))"
shows "∀B. ( B ⊆ X⇩2 ⟶ cl⇩1(f-(B)) ⊆ f-(cl⇩2(B)) )"
proof -
{ fix B assume "B ⊆ X⇩2"
from fmapAssum A1 have "f(cl⇩1(f-(B))) ⊆ cl⇩2(f(f-(B)))"
using func1_1_L3 by simp
moreover from fmapAssum ‹B ⊆ X⇩2› have "cl⇩2(f(f-(B))) ⊆ cl⇩2(B)"
using fun_is_function function_image_vimage func1_1_L6
topol_cntxs_valid topology0.top_closure_mono
by simp
ultimately have "f-(f(cl⇩1(f-(B)))) ⊆ f-(cl⇩2(B))"
using fmapAssum fun_is_function by auto
moreover from fmapAssum ‹B ⊆ X⇩2› have
"cl⇩1(f-(B)) ⊆ f-(f(cl⇩1(f-(B))))"
using func1_1_L3 func1_1_L9 IsClosed_def
topol_cntxs_valid topology0.cl_is_closed by simp
ultimately have "cl⇩1(f-(B)) ⊆ f-(cl⇩2(B))" by auto
} then show ?thesis by simp
qed

text‹If $\overline{f^{-1}(B)}\subseteq f^{-1}\left( \overline{B} \right)$
(the inverse image of a closure contains the closure of the
inverse image), then the function is continuous. This lemma closes a series of
implications in lemmas  ‹ Top_ZF_2_1_L1›,
‹ Top_ZF_2_1_L2› and ‹ Top_ZF_2_1_L3› showing equivalence
of four definitions of continuity.›

lemma (in two_top_spaces0) Top_ZF_2_1_L4:
assumes A1: "∀B. ( B ⊆ X⇩2 ⟶ cl⇩1(f-(B)) ⊆ f-(cl⇩2(B)) )"
shows "f {is continuous}"
proof -
{ fix U assume "U ∈ τ⇩2"
then have "(X⇩2 - U) {is closed in} τ⇩2"
using topol_cntxs_valid topology0.Top_3_L9 by simp
moreover have "X⇩2 - U ⊆ ⋃τ⇩2" by auto
ultimately have "cl⇩2(X⇩2 - U) = X⇩2 - U"
using topol_cntxs_valid topology0.Top_3_L8 by simp
moreover from A1 have "cl⇩1(f-(X⇩2 - U)) ⊆ f-(cl⇩2(X⇩2 - U))"
by auto
ultimately have "cl⇩1(f-(X⇩2 - U)) ⊆ f-(X⇩2 - U)" by simp
moreover from fmapAssum have "f-(X⇩2 - U) ⊆ cl⇩1(f-(X⇩2 - U))"
using func1_1_L3 topol_cntxs_valid topology0.cl_contains_set
by simp
ultimately have "f-(X⇩2 - U) {is closed in} τ⇩1"
using fmapAssum func1_1_L3 topol_cntxs_valid topology0.Top_3_L8
by auto
with fmapAssum have "f-(U) ∈ τ⇩1"
using fun_is_function function_vimage_Diff func1_1_L4
func1_1_L3 IsClosed_def double_complement by simp
} then have "∀U∈τ⇩2. f-(U) ∈ τ⇩1" by simp
then show ?thesis using IsContinuous_def by simp
qed

text‹For continuous functions the closure of the inverse image is contained in the
inverse image of the closure. This is a shortcut through a series of implications
provided by ‹TopZF_2_1_L1›, ‹Top_ZF_2_1_L2› and ‹Top_ZF_2_1_L3›. ›

corollary (in two_top_spaces0) im_cl_in_cl_im:
assumes "f {is continuous}" and "B ⊆ X⇩2"
shows "cl⇩1(f-(B)) ⊆ f-(cl⇩2(B))"
using assms TopZF_2_1_L1 Top_ZF_2_1_L2 Top_ZF_2_1_L3 by simp

text‹Another condition for continuity: it is sufficient to check if the
inverse image of every set in a base is open.›

lemma (in two_top_spaces0) Top_ZF_2_1_L5:
assumes A1: "B {is a base for} τ⇩2" and A2: "∀U∈B. f-(U) ∈ τ⇩1"
shows "f {is continuous}"
proof -
{ fix V assume A3: "V ∈ τ⇩2"
with A1 obtain A where "A ⊆ B"  "V = ⋃A"
using IsAbaseFor_def by auto
with A2 have "{f-(U). U∈A} ⊆ τ⇩1" by auto
with tau1_is_top have "⋃ {f-(U). U∈A} ∈ τ⇩1"
using IsATopology_def by simp
moreover from ‹A ⊆ B› ‹V = ⋃A› have "f-(V) = ⋃{f-(U). U∈A}"
by auto
ultimately have "f-(V) ∈  τ⇩1" by simp
} then show "f {is continuous}" using IsContinuous_def
by simp
qed

text‹We can strenghten the previous lemma: it is sufficient to check if the
inverse image of every set in a subbase is open. The proof is rather awkward,
as usual when we deal with general intersections. We have to keep track of
the case when the collection is empty.›

lemma (in two_top_spaces0) Top_ZF_2_1_L6:
assumes A1: "B {is a subbase for} τ⇩2" and A2: "∀U∈B. f-(U) ∈ τ⇩1"
shows "f {is continuous}"
proof -
let ?C = "{⋂A. A ∈ FinPow(B)}"
from A1 have "?C {is a base for} τ⇩2"
using IsAsubBaseFor_def by simp
moreover have "∀U∈?C. f-(U) ∈ τ⇩1"
proof
fix U assume "U∈?C"
{ assume "f-(U) = 0"
with tau1_is_top have "f-(U) ∈ τ⇩1"
using empty_open by simp }
moreover
{ assume "f-(U) ≠ 0"
then have "U≠0" by (rule func1_1_L13)
moreover from ‹U∈?C› obtain A where
"A ∈ FinPow(B)" and "U = ⋂A"
by auto
ultimately have "⋂A≠0" by simp
then have "A≠0" by (rule inter_nempty_nempty)
then have "{f-(W). W∈A} ≠ 0" by simp
moreover from A2 ‹A ∈ FinPow(B)› have "{f-(W). W∈A} ∈ FinPow(τ⇩1)"
by (rule fin_image_fin)
ultimately have "⋂{f-(W). W∈A} ∈ τ⇩1"
using topol_cntxs_valid topology0.fin_inter_open_open by simp
moreover
from ‹A ∈ FinPow(B)› have "A ⊆ B" using FinPow_def by simp
with tau2_is_top A1 have "A ⊆ Pow(X⇩2)"
using IsAsubBaseFor_def IsATopology_def by auto
with fmapAssum ‹A≠0› ‹U = ⋂A› have "f-(U) = ⋂{f-(W). W∈A}"
using func1_1_L12 by simp
ultimately have "f-(U) ∈ τ⇩1" by simp }
ultimately show "f-(U) ∈ τ⇩1" by blast
qed
ultimately show "f {is continuous}"
using Top_ZF_2_1_L5 by simp
qed

text‹A dual of ‹ Top_ZF_2_1_L5›: a function that maps base sets to open sets
is open.›

lemma (in two_top_spaces0) base_image_open:
assumes A1: "ℬ {is a base for} τ⇩1" and A2: "∀B∈ℬ. f(B) ∈ τ⇩2" and A3: "U∈τ⇩1"
shows "f(U) ∈ τ⇩2"
proof -
from A1 A3 obtain ℰ where "ℰ ∈ Pow(ℬ)" and "U = ⋃ℰ" using Top_1_2_L1 by blast
with A1 have "f(U) = ⋃{f(E). E ∈ ℰ}" using Top_1_2_L5  fmapAssum image_of_Union
by auto
moreover
from A2 ‹ℰ ∈ Pow(ℬ)› have "{f(E). E ∈ ℰ} ∈ Pow(τ⇩2)" by auto
then have "⋃{f(E). E ∈ ℰ} ∈ τ⇩2" using tau2_is_top IsATopology_def by simp
ultimately show ?thesis using tau2_is_top IsATopology_def by auto
qed

text‹A composition of two continuous functions is continuous.›

lemma comp_cont: assumes "IsContinuous(T,S,f)" and "IsContinuous(S,R,g)"
shows "IsContinuous(T,R,g O f)"
using assms IsContinuous_def vimage_comp by simp

text‹A composition of three continuous functions is continuous.›

lemma comp_cont3:
assumes "IsContinuous(T,S,f)" and "IsContinuous(S,R,g)" and "IsContinuous(R,P,h)"
shows "IsContinuous(T,P,h O g O f)"
using assms IsContinuous_def vimage_comp by simp

text‹The graph of a continuous function into a Hausdorff topological space is closed
in the product topology. Recall that in ZF a function is the same as its graph.›

lemma (in two_top_spaces0) into_T2_graph_closed:
assumes "f {is continuous}" "τ⇩2 {is T⇩2}"
shows "f {is closed in} ProductTopology(τ⇩1,τ⇩2)"
proof -
from fmapAssum have "f = {⟨x,f(x)⟩. x∈X⇩1}" using fun_is_set_of_pairs
by simp
let ?f⇩c = "X⇩1×X⇩2 - f"
have "?f⇩c ∈ ProductTopology(τ⇩1,τ⇩2)"
proof -
{ fix p assume "p∈?f⇩c"
then have "p ∈ X⇩1×X⇩2" and "p ∉ f" by auto
from ‹p∈X⇩1×X⇩2› obtain x y where "x∈X⇩1" "y∈X⇩2" "p = ⟨x,y⟩"
by auto
have "y≠f(x)"
proof -
{ assume "y=f(x)"
with ‹x∈X⇩1› ‹p = ⟨x,y⟩› have "p ∈ {⟨x,f(x)⟩. x∈X⇩1}" by auto
with ‹f = {⟨x,f(x)⟩. x∈X⇩1}› ‹p ∉ f› have False by auto
} thus "y≠f(x)" by auto
qed
from fmapAssum ‹x∈X⇩1› have "f(x) ∈ X⇩2" by (rule apply_funtype)
with ‹y∈X⇩2›  have "y∈⋃τ⇩2" "f(x) ∈ ⋃τ⇩2" by auto
with assms(2) ‹y≠f(x)› obtain U V
where "U∈τ⇩2" "V∈τ⇩2" "y∈U" "f(x)∈V" "U∩V = 0"
unfolding isT2_def by blast
let ?W = "f-(V)"
have "?W∈τ⇩1" "?W⊆X⇩1" "U⊆X⇩2" "x∈?W" "p∈?W×U" "f(?W) ⊆ V"
proof -
from assms(1) have "IsContinuous(τ⇩1,τ⇩2,f)" by simp
with ‹V∈τ⇩2› ‹U∈τ⇩2› show "?W∈τ⇩1" "?W⊆X⇩1" "U⊆X⇩2"
unfolding IsContinuous_def by auto
from fmapAssum ‹x∈X⇩1› ‹f(x)∈V› show "x∈?W" using func1_1_L15
by auto
with ‹y∈U› ‹y∈U› ‹p = ⟨x,y⟩› show  "p∈?W×U" by simp
from fmapAssum show "f(?W) ⊆ V"
using fun_is_fun function_image_vimage by simp
qed
from fmapAssum ‹U∩V = 0› ‹?W⊆X⇩1› ‹U⊆X⇩2› have "?W×U ⊆ ?f⇩c"
using vimage_prod_dis_graph by blast
with ‹?W∈τ⇩1› ‹U∈τ⇩2› ‹p∈?W×U› have "∃W∈τ⇩1.∃U∈τ⇩2. p∈W×U ∧ W×U ⊆ ?f⇩c"
by blast
}
with tau1_is_top tau2_is_top show "?f⇩c ∈ ProductTopology(τ⇩1,τ⇩2)"
using point_neighb_prod_top by simp
qed
with fmapAssum tau1_is_top tau2_is_top show ?thesis
using fun_subset_prod Top_1_4_T1(3) unfolding IsClosed_def
by auto
qed

subsection‹Homeomorphisms›

text‹This section studies ''homeomorphisms'' - continous bijections whose inverses
are also continuous. Notions that are preserved by (commute with)
homeomorphisms are called ''topological invariants''.›

text‹Homeomorphism is a bijection that preserves open sets.›

definition "IsAhomeomorphism(T,S,f) ≡
f ∈ bij(⋃T,⋃S) ∧ IsContinuous(T,S,f) ∧ IsContinuous(S,T,converse(f))"

text‹Inverse (converse) of a homeomorphism is a homeomorphism.›

lemma homeo_inv: assumes "IsAhomeomorphism(T,S,f)"
shows "IsAhomeomorphism(S,T,converse(f))"
using assms IsAhomeomorphism_def bij_converse_bij bij_converse_converse
by auto

text‹Homeomorphisms are open maps.›

lemma homeo_open: assumes "IsAhomeomorphism(T,S,f)" and "U∈T"
shows "f(U) ∈ S"
using assms image_converse IsAhomeomorphism_def IsContinuous_def by simp

text‹A continuous bijection that is an open map is a homeomorphism.›

lemma bij_cont_open_homeo:
assumes "f ∈ bij(⋃T,⋃S)" and "IsContinuous(T,S,f)" and "∀U∈T. f(U) ∈ S"
shows "IsAhomeomorphism(T,S,f)"
using assms image_converse IsAhomeomorphism_def IsContinuous_def by auto

text‹A continuous bijection that maps base to open sets is a homeomorphism.›

lemma (in two_top_spaces0) bij_base_open_homeo:
assumes A1: "f ∈ bij(X⇩1,X⇩2)" and A2: "ℬ {is a base for} τ⇩1"  and A3: "𝒞 {is a base for} τ⇩2" and
A4: "∀U∈𝒞. f-(U) ∈ τ⇩1" and A5: "∀V∈ℬ. f(V) ∈ τ⇩2"
shows "IsAhomeomorphism(τ⇩1,τ⇩2,f)"
using assms tau2_is_top tau1_is_top bij_converse_bij bij_is_fun two_top_spaces0_def
image_converse two_top_spaces0.Top_ZF_2_1_L5 IsAhomeomorphism_def by simp

text‹A bijection that maps base to base is a homeomorphism.›

lemma (in two_top_spaces0) bij_base_homeo:
assumes A1: "f ∈ bij(X⇩1,X⇩2)" and A2: "ℬ {is a base for} τ⇩1" and
A3: "{f(B). B∈ℬ} {is a base for} τ⇩2"
shows "IsAhomeomorphism(τ⇩1,τ⇩2,f)"
proof -
note A1
moreover have "f {is continuous}"
proof -
{ fix C assume "C ∈ {f(B). B∈ℬ}"
then obtain B where "B∈ℬ" and I: "C = f(B)" by auto
with A2 have "B ⊆ X⇩1" using Top_1_2_L5 by auto
with A1 A2 ‹B∈ℬ› I have "f-(C) ∈ τ⇩1"
using bij_def inj_vimage_image base_sets_open by auto
} hence "∀C ∈ {f(B). B∈ℬ}. f-(C) ∈ τ⇩1" by auto
with A3 show ?thesis by (rule Top_ZF_2_1_L5)
qed
moreover
from A3 have "∀B∈ℬ. f(B) ∈ τ⇩2" using base_sets_open by auto
with A2 have "∀U∈τ⇩1. f(U) ∈ τ⇩2" using base_image_open by simp
ultimately show ?thesis using bij_cont_open_homeo by simp
qed

text‹Interior is a topological invariant.›

theorem int_top_invariant: assumes A1: "A⊆⋃T" and A2: "IsAhomeomorphism(T,S,f)"
shows "f(Interior(A,T)) = Interior(f(A),S)"
proof -
let ?𝒜 = "{U∈T. U⊆A}"
have I: "{f(U). U∈?𝒜} = {V∈S. V ⊆ f(A)}"
proof
from A2 show "{f(U). U∈?𝒜} ⊆ {V∈S. V ⊆ f(A)}"
using homeo_open by auto
{ fix V assume "V ∈ {V∈S. V ⊆ f(A)}"
hence "V∈S" and II: "V ⊆ f(A)" by auto
let ?U = "f-(V)"
from II have "?U ⊆ f-(f(A))" by auto
moreover from assms have "f-(f(A)) = A"
using IsAhomeomorphism_def bij_def inj_vimage_image by auto
moreover from A2 ‹V∈S› have "?U∈T"
using IsAhomeomorphism_def IsContinuous_def by simp
moreover
from ‹V∈S› have "V ⊆ ⋃S" by auto
with A2 have "V = f(?U)"
using IsAhomeomorphism_def bij_def surj_image_vimage by auto
ultimately have "V ∈ {f(U). U∈?𝒜}" by auto
} thus "{V∈S. V ⊆ f(A)} ⊆ {f(U). U∈?𝒜}" by auto
qed
have "f(Interior(A,T)) =  f(⋃?𝒜)" unfolding Interior_def by simp
also from A2 have "… = ⋃{f(U). U∈?𝒜}"
using IsAhomeomorphism_def bij_def inj_def image_of_Union by auto
also from I have "… = Interior(f(A),S)" unfolding Interior_def by simp
finally show ?thesis by simp
qed

subsection‹Topologies induced by mappings›

text‹In this section we consider various ways a topology may be defined on a set that
is the range (or the domain) of a function whose domain (or range) is a topological space.
›

text‹A bijection from a topological space induces a topology on the range.›

theorem bij_induced_top: assumes A1: "T {is a topology}" and A2: "f ∈ bij(⋃T,Y)"
shows
"{f(U). U∈T} {is a topology}" and
"{ {f(x).x∈U}. U∈T} {is a topology}" and
"(⋃{f(U). U∈T}) = Y" and
"IsAhomeomorphism(T, {f(U). U∈T},f)"
proof -
from A2 have "f ∈ inj(⋃T,Y)" using bij_def by simp
then have "f:⋃T→Y" using inj_def by simp
let ?S = "{f(U). U∈T}"
{ fix M assume "M ∈ Pow(?S)"
let ?M⇩T = "{f-(V). V∈M}"
have "?M⇩T ⊆ T"
proof
fix W assume "W∈?M⇩T"
then obtain V where "V∈M" and I: "W = f-(V)" by auto
with ‹M ∈ Pow(?S)› have "V∈?S" by auto
then obtain U where "U∈T" and  "V = f(U)" by auto
with I have "W = f-(f(U))" by simp
with ‹f ∈ inj(⋃T,Y)›  ‹U∈T› have "W = U" using inj_vimage_image by blast
with ‹U∈T› show "W∈T" by simp
qed
with A1 have "(⋃?M⇩T) ∈ T" using IsATopology_def by simp
hence "f(⋃?M⇩T) ∈  ?S" by auto
moreover have "f(⋃?M⇩T) = ⋃M"
proof -
from ‹f:⋃T→Y› ‹?M⇩T ⊆ T›  have "f(⋃?M⇩T) = ⋃{f(U). U∈?M⇩T}"
using image_of_Union by auto
moreover have "{f(U). U∈?M⇩T} = M"
proof -
from ‹f:⋃T→Y› have "∀U∈T. f(U) ⊆ Y" using  func1_1_L6 by simp
with ‹M ∈ Pow(?S)› have "M ⊆ Pow(Y)" by auto
with A2 show "{f(U). U∈?M⇩T} = M" using bij_def surj_subsets by auto
qed
ultimately show "f(⋃?M⇩T) = ⋃M" by simp
qed
ultimately have "⋃M ∈ ?S" by auto
} then have "∀M∈Pow(?S). ⋃M ∈ ?S" by auto
moreover
{ fix U V assume "U∈?S" "V∈?S"
then obtain U⇩T V⇩T where "U⇩T ∈ T"   "V⇩T ∈ T" and
I: "U = f(U⇩T)"  "V = f(V⇩T)"
by auto
with A1 have "U⇩T∩V⇩T ∈ T" using IsATopology_def by simp
hence "f(U⇩T∩V⇩T) ∈ ?S" by auto
moreover have "f(U⇩T∩V⇩T) = U∩V"
proof -
from ‹U⇩T ∈ T›  ‹V⇩T ∈ T› have "U⇩T ⊆ ⋃T"  "V⇩T ⊆ ⋃T"
using bij_def by auto
with ‹f ∈ inj(⋃T,Y)› I show "f(U⇩T∩V⇩T) = U∩V" using inj_image_inter
by simp
qed
ultimately have "U∩V ∈ ?S" by simp
} then have "∀U∈?S. ∀V∈?S. U∩V ∈ ?S" by auto
ultimately show "?S {is a topology}" using IsATopology_def by simp
moreover from ‹f:⋃T→Y› have "∀U∈T. f(U) = {f(x).x∈U}"
using func_imagedef by blast
ultimately show "{ {f(x).x∈U}. U∈T} {is a topology}" by simp
show "⋃?S =  Y"
proof
from ‹f:⋃T→Y› have "∀U∈T. f(U) ⊆ Y" using func1_1_L6 by simp
thus "⋃?S ⊆ Y" by auto
from A1 have "f(⋃T) ⊆ ⋃?S" using IsATopology_def by auto
with A2 show "Y ⊆ ⋃?S" using bij_def surj_range_image_domain
by auto
qed
show "IsAhomeomorphism(T,?S,f)"
proof -
from A2  ‹⋃?S =  Y› have "f ∈ bij(⋃T,⋃?S)" by simp
moreover have "IsContinuous(T,?S,f)"
proof -
{ fix V assume "V∈?S"
then obtain U where "U∈T" and "V = f(U)" by auto
hence "U ⊆ ⋃T" and "f-(V) = f-(f(U))"  by auto
with ‹f ∈ inj(⋃T,Y)›  ‹U∈T› have "f-(V) ∈ T"  using inj_vimage_image
by simp
} then show "IsContinuous(T,?S,f)" unfolding IsContinuous_def by auto
qed
ultimately show"IsAhomeomorphism(T,?S,f)" using bij_cont_open_homeo
by auto
qed
qed

subsection‹Partial functions and continuity›

text‹Suppose we have two topologies $\tau_1,\tau_2$ on sets
$X_i=\bigcup\tau_i, i=1,2$. Consider some function $f:A\rightarrow X_2$, where
$A\subseteq X_1$ (we will call such function ''partial''). In such situation we have two
natural possibilities for the pairs of topologies with respect to which this function may
be continuous. One is obviously the original $\tau_1,\tau_2$ and in the second one
the first element of the pair is the topology relative to the domain of the
function: $\{A\cap U | U \in \tau_1\}$. These two possibilities are not exactly
the same and the goal of this section is to explore the differences.›

text‹If a function is continuous, then its restriction is continous in relative
topology.›

lemma (in two_top_spaces0) restr_cont:
assumes A1: "A ⊆ X⇩1" and A2: "f {is continuous}"
shows "IsContinuous(τ⇩1 {restricted to} A, τ⇩2,restrict(f,A))"
proof -
let ?g = "restrict(f,A)"
{ fix U assume "U ∈ τ⇩2"
with A2 have "f-(U) ∈ τ⇩1" using IsContinuous_def by simp
moreover from A1 have "?g-(U) = f-(U) ∩ A"
using fmapAssum func1_2_L1 by simp
ultimately have "?g-(U) ∈ (τ⇩1 {restricted to} A)"
using RestrictedTo_def by auto
} then show ?thesis using IsContinuous_def by simp
qed

text‹If a function is continuous, then it is continuous when we restrict
the topology on the range to the image of the domain.›

lemma (in two_top_spaces0) restr_image_cont:
assumes A1: "f {is continuous}"
shows "IsContinuous(τ⇩1, τ⇩2 {restricted to} f(X⇩1),f)"
proof -
have "∀U ∈ τ⇩2 {restricted to} f(X⇩1). f-(U) ∈ τ⇩1"
proof
fix U assume "U ∈ τ⇩2 {restricted to} f(X⇩1)"
then obtain V where "V ∈ τ⇩2" and "U = V ∩ f(X⇩1)"
using RestrictedTo_def by auto
with A1 show  "f-(U) ∈ τ⇩1"
using fmapAssum inv_im_inter_im IsContinuous_def
by simp
qed
then show ?thesis using IsContinuous_def by simp
qed

text‹A combination of ‹restr_cont› and ‹restr_image_cont›.›

lemma (in two_top_spaces0) restr_restr_image_cont:
assumes A1: "A ⊆ X⇩1" and A2: "f {is continuous}" and
A3: "g = restrict(f,A)" and
A4: "τ⇩3 = τ⇩1 {restricted to} A"
shows "IsContinuous(τ⇩3, τ⇩2 {restricted to} g(A),g)"
proof -
from A1 A4 have "⋃τ⇩3 = A"
using union_restrict by auto
have "two_top_spaces0(τ⇩3, τ⇩2, g)"
proof -
from A4 have
"τ⇩3 {is a topology}" and "τ⇩2 {is a topology}"
using tau1_is_top tau2_is_top
topology0_def topology0.Top_1_L4 by auto
moreover from A1 A3 ‹⋃τ⇩3 = A› have "g: ⋃τ⇩3 → ⋃τ⇩2"
using fmapAssum restrict_type2 by simp
ultimately show ?thesis using two_top_spaces0_def
by simp
qed
moreover from assms have "IsContinuous(τ⇩3, τ⇩2, g)"
using restr_cont by simp
ultimately have "IsContinuous(τ⇩3, τ⇩2 {restricted to} g(⋃τ⇩3),g)"
by (rule two_top_spaces0.restr_image_cont)
moreover note ‹⋃τ⇩3 = A›
ultimately show ?thesis by simp
qed

text‹We need a context similar to ‹two_top_spaces0› but without
the global function $f:X_1\rightarrow X_2$.›

locale two_top_spaces1 =

fixes τ⇩1
assumes tau1_is_top: "τ⇩1 {is a topology}"

fixes τ⇩2
assumes tau2_is_top: "τ⇩2 {is a topology}"

fixes X⇩1
defines X1_def [simp]: "X⇩1 ≡ ⋃τ⇩1"

fixes X⇩2
defines X2_def [simp]: "X⇩2 ≡ ⋃τ⇩2"

text‹If a partial function $g:X_1\supseteq A\rightarrow X_2$ is continuous with
respect to $(\tau_1,\tau_2)$, then $A$ is open (in $\tau_1$) and
the function is continuous in the relative topology.›

lemma (in two_top_spaces1) partial_fun_cont:
assumes A1: "g:A→X⇩2" and A2: "IsContinuous(τ⇩1,τ⇩2,g)"
shows "A ∈ τ⇩1" and "IsContinuous(τ⇩1 {restricted to} A, τ⇩2, g)"
proof -
from A2 have "g-(X⇩2) ∈ τ⇩1"
using tau2_is_top IsATopology_def IsContinuous_def by simp
with A1 show "A ∈ τ⇩1" using func1_1_L4 by simp
{ fix V assume "V ∈ τ⇩2"
with A2 have "g-(V) ∈ τ⇩1" using IsContinuous_def by simp
moreover
from A1 have "g-(V) ⊆ A" using func1_1_L3 by simp
hence "g-(V) = A ∩ g-(V)" by auto
ultimately have "g-(V) ∈ (τ⇩1 {restricted to} A)"
using RestrictedTo_def by auto
} then show "IsContinuous(τ⇩1 {restricted to} A, τ⇩2, g)"
using IsContinuous_def by simp
qed

text‹For partial function defined on open sets continuity in the whole
and relative topologies are the same.›

lemma (in two_top_spaces1) part_fun_on_open_cont:
assumes A1: "g:A→X⇩2" and A2: "A ∈ τ⇩1"
shows "IsContinuous(τ⇩1,τ⇩2,g) ⟷
IsContinuous(τ⇩1 {restricted to} A, τ⇩2, g)"
proof
assume "IsContinuous(τ⇩1,τ⇩2,g)"
with A1 show "IsContinuous(τ⇩1 {restricted to} A, τ⇩2, g)"
using partial_fun_cont by simp
next
assume I: "IsContinuous(τ⇩1 {restricted to} A, τ⇩2, g)"
{ fix V assume "V ∈ τ⇩2"
with I have "g-(V) ∈ (τ⇩1 {restricted to} A)"
using IsContinuous_def by simp
then obtain W where "W ∈ τ⇩1" and "g-(V) = A∩W"
using RestrictedTo_def by auto
with A2 have "g-(V) ∈ τ⇩1" using tau1_is_top IsATopology_def
by simp
} then show "IsContinuous(τ⇩1,τ⇩2,g)" using IsContinuous_def
by simp
qed

subsection‹Product topology and continuity›

text‹We start with three topological spaces $(\tau_1,X_1), (\tau_2,X_2)$ and
$(\tau_3,X_3)$ and a function $f:X_1\times X_2\rightarrow X_3$. We will study
the properties of $f$ with respect to the product topology $\tau_1\times \tau_2$
and $\tau_3$. This situation is similar as in locale ‹two_top_spaces0›
but the first topological space is assumed to be a product of two topological spaces.
›

text‹First we define a locale with three topological spaces.›

locale prod_top_spaces0 =

fixes τ⇩1
assumes tau1_is_top: "τ⇩1 {is a topology}"

fixes τ⇩2
assumes tau2_is_top: "τ⇩2 {is a topology}"

fixes τ⇩3
assumes tau3_is_top: "τ⇩3 {is a topology}"

fixes X⇩1
defines X1_def [simp]: "X⇩1 ≡ ⋃τ⇩1"

fixes X⇩2
defines X2_def [simp]: "X⇩2 ≡ ⋃τ⇩2"

fixes X⇩3
defines X3_def [simp]: "X⇩3 ≡ ⋃τ⇩3"

fixes η
defines eta_def [simp]: "η ≡ ProductTopology(τ⇩1,τ⇩2)"

text‹Fixing the first variable in a two-variable continuous function results in a
continuous function.›

lemma (in prod_top_spaces0) fix_1st_var_cont:
assumes "f: X⇩1×X⇩2→X⇩3" and "IsContinuous(η,τ⇩3,f)"
and "x∈X⇩1"
shows "IsContinuous(τ⇩2,τ⇩3,Fix1stVar(f,x))"
using assms fix_1st_var_vimage IsContinuous_def tau1_is_top tau2_is_top
prod_sec_open1 by simp

text‹Fixing the second variable in a two-variable continuous function results in a
continuous function.›

lemma (in prod_top_spaces0) fix_2nd_var_cont:
assumes "f: X⇩1×X⇩2→X⇩3" and "IsContinuous(η,τ⇩3,f)"
and "y∈X⇩2"
shows "IsContinuous(τ⇩1,τ⇩3,Fix2ndVar(f,y))"
using assms fix_2nd_var_vimage IsContinuous_def tau1_is_top tau2_is_top
prod_sec_open2 by simp

text‹Having two constinuous mappings we can construct a third one on the cartesian product
of the domains.›

lemma cart_prod_cont:
assumes A1: "τ⇩1 {is a topology}" "τ⇩2 {is a topology}" and
A2: "η⇩1 {is a topology}" "η⇩2 {is a topology}" and
A3a: "f⇩1:⋃τ⇩1→⋃η⇩1"  and A3b: "f⇩2:⋃τ⇩2→⋃η⇩2" and
A4: "IsContinuous(τ⇩1,η⇩1,f⇩1)" "IsContinuous(τ⇩2,η⇩2,f⇩2)" and
A5: "g = {⟨p,⟨f⇩1(fst(p)),f⇩2(snd(p))⟩⟩. p ∈ ⋃τ⇩1×⋃τ⇩2}"
shows "IsContinuous(ProductTopology(τ⇩1,τ⇩2),ProductTopology(η⇩1,η⇩2),g)"
proof -
let ?τ = "ProductTopology(τ⇩1,τ⇩2)"
let ?η = "ProductTopology(η⇩1,η⇩2)"
let ?X⇩1 = "⋃τ⇩1"
let ?X⇩2 = "⋃τ⇩2"
let ?Y⇩1 = "⋃η⇩1"
let ?Y⇩2 = "⋃η⇩2"
let ?B = "ProductCollection(η⇩1,η⇩2)"
from A1 A2 have "?τ {is a topology}" and "?η {is a topology}"
using Top_1_4_T1 by auto
moreover have "g: ?X⇩1×?X⇩2 → ?Y⇩1×?Y⇩2"
proof -
{ fix p assume "p ∈ ?X⇩1×?X⇩2"
hence "fst(p) ∈ ?X⇩1" and "snd(p) ∈ ?X⇩2" by auto
from A3a ‹fst(p) ∈ ?X⇩1› have "f⇩1(fst(p)) ∈ ?Y⇩1"
by (rule apply_funtype)
moreover from A3b ‹snd(p) ∈ ?X⇩2› have "f⇩2(snd(p)) ∈ ?Y⇩2"
by (rule apply_funtype)
ultimately have "⟨f⇩1(fst(p)),f⇩2(snd(p))⟩ ∈ ⋃η⇩1×⋃η⇩2" by auto
} hence "∀p ∈ ?X⇩1×?X⇩2. ⟨f⇩1(fst(p)),f⇩2(snd(p))⟩ ∈ ?Y⇩1×?Y⇩2"
by simp
with A5 show "g: ?X⇩1×?X⇩2 → ?Y⇩1×?Y⇩2" using ZF_fun_from_total
by simp
qed
moreover from A1 A2 have "⋃?τ = ?X⇩1×?X⇩2" and "⋃?η = ?Y⇩1×?Y⇩2"
using Top_1_4_T1 by auto
ultimately have "two_top_spaces0(?τ,?η,g)" using two_top_spaces0_def
by simp
moreover from A2 have "?B {is a base for} ?η" using Top_1_4_T1
by simp
moreover have "∀U∈?B. g-(U) ∈ ?τ"
proof
fix U assume "U∈?B"
then obtain V W where "V ∈ η⇩1" "W ∈ η⇩2" and "U = V×W"
using ProductCollection_def by auto
with A3a A3b A5 have "g-(U) = f⇩1-(V) × f⇩2-(W)"
using cart_prod_fun_vimage by simp
moreover from A1 A4 ‹V ∈ η⇩1› ‹W ∈ η⇩2› have "f⇩1-(V) × f⇩2-(W) ∈ ?τ"
using IsContinuous_def prod_open_open_prod by simp
ultimately show "g-(U) ∈ ?τ" by simp
qed
ultimately show ?thesis using two_top_spaces0.Top_ZF_2_1_L5
by simp
qed

text‹A reformulation of the ‹cart_prod_cont› lemma above in slightly different notation.›

theorem (in two_top_spaces0) product_cont_functions:
assumes "f:X⇩1→X⇩2" "g:⋃τ⇩3→⋃τ⇩4"
"IsContinuous(τ⇩1,τ⇩2,f)" "IsContinuous(τ⇩3,τ⇩4,g)"
"τ⇩4{is a topology}" "τ⇩3{is a topology}"
shows "IsContinuous(ProductTopology(τ⇩1,τ⇩3),ProductTopology(τ⇩2,τ⇩4),{⟨⟨x,y⟩,⟨fx,gy⟩⟩. ⟨x,y⟩∈X⇩1×⋃τ⇩3})"
proof -
have "{⟨⟨x,y⟩,⟨fx,gy⟩⟩. ⟨x,y⟩∈X⇩1×⋃τ⇩3} = {⟨p,⟨f(fst(p)),g(snd(p))⟩⟩. p ∈ X⇩1×⋃τ⇩3}"
by force
with tau1_is_top tau2_is_top assms show ?thesis using cart_prod_cont by simp
qed

text‹A special case of ‹cart_prod_cont› when the function acting on the second
axis is the identity.›

lemma cart_prod_cont1:
assumes A1: "τ⇩1 {is a topology}" and A1a: "τ⇩2 {is a topology}" and
A2: "η⇩1 {is a topology}"  and
A3: "f⇩1:⋃τ⇩1→⋃η⇩1" and A4: "IsContinuous(τ⇩1,η⇩1,f⇩1)" and
A5: "g = {⟨p, ⟨f⇩1(fst(p)),snd(p)⟩⟩. p ∈ ⋃τ⇩1×⋃τ⇩2}"
shows "IsContinuous(ProductTopology(τ⇩1,τ⇩2),ProductTopology(η⇩1,τ⇩2),g)"
proof -
let ?f⇩2 = "id(⋃τ⇩2)"
have "∀x∈⋃τ⇩2. ?f⇩2(x) = x" using id_conv by blast
hence I: "∀p ∈ ⋃τ⇩1×⋃τ⇩2. snd(p) = ?f⇩2(snd(p))" by simp
note A1 A1a A2 A1a A3
moreover have "?f⇩2:⋃τ⇩2→⋃τ⇩2"  using id_type by simp
moreover note A4
moreover have "IsContinuous(τ⇩2,τ⇩2,?f⇩2)" using id_cont by simp
moreover have "g = {⟨p, ⟨f⇩1(fst(p)),?f⇩2(snd(p))⟩ ⟩. p ∈ ⋃τ⇩1×⋃τ⇩2}"
proof
from A5 I show  "g ⊆ {⟨p, ⟨f⇩1(fst(p)),?f⇩2(snd(p))⟩⟩. p ∈ ⋃τ⇩1×⋃τ⇩2}"
by auto
from A5 I show "{⟨p, ⟨f⇩1(fst(p)),?f⇩2(snd(p))⟩⟩. p ∈ ⋃τ⇩1×⋃τ⇩2} ⊆ g"
by auto
qed
ultimately show ?thesis by (rule cart_prod_cont)
qed

text‹Having two continuous mappings $f,g$ we can construct a third one with values
in the cartesian product of the codomains of $f,g$,
defined by $x\mapsto \langle f(x),g(x) \rangle$. ›

lemma (in prod_top_spaces0) cont_funcs_prod:
assumes "f:X⇩1→X⇩2" "g:X⇩1→X⇩3" "IsContinuous(τ⇩1,τ⇩2,f)" "IsContinuous(τ⇩1,τ⇩3,g)"
defines "h ≡ {⟨x,⟨f(x),g(x)⟩⟩. x∈X⇩1}"
shows "IsContinuous(τ⇩1,ProductTopology(τ⇩2,τ⇩3),h)"
proof -
let ?B = "ProductCollection(τ⇩2,τ⇩3)"
have
"two_top_spaces0(τ⇩1,ProductTopology(τ⇩2,τ⇩3),h)"
"?B {is a base for} ProductTopology(τ⇩2,τ⇩3)"
"∀W∈?B. h-(W) ∈ τ⇩1"
proof -
from tau1_is_top tau2_is_top tau3_is_top assms(1,2,5)
show "two_top_spaces0(τ⇩1,ProductTopology(τ⇩2,τ⇩3),h)"
using vimage_prod Top_1_4_T1(1,3) unfolding two_top_spaces0_def
by simp
from tau2_is_top tau3_is_top show"?B {is a base for} ProductTopology(τ⇩2,τ⇩3)"
using Top_1_4_T1(2) by simp
from tau1_is_top assms show "∀W∈?B. h-(W) ∈ τ⇩1"
unfolding ProductCollection_def IsContinuous_def IsATopology_def
using vimage_prod by simp
qed
then show ?thesis by (rule two_top_spaces0.Top_ZF_2_1_L5)
qed

text‹Having two continuous mappings $f,g$ we can construct a third one with values
in the cartesian product of the codomains of $f,g$,
defined by $x\mapsto \langle f(x),g(x) \rangle$. This is essentially the same as
‹cont_funcs_prod› but formulated in a way that is sometimes easier to apply.
Recall that $\tau_2 \times_t \tau_3$ is a notation for the product topology
of $\tau_1$ and $\tau_2$.  ›

lemma cont_funcs_prod1:
assumes "τ⇩1 {is a topology}" "τ⇩2 {is a topology}" "τ⇩3 {is a topology}" and
"{⟨x,p(x)⟩. x∈⋃τ⇩1} ∈ Cont(τ⇩1,τ⇩2)" "{⟨x,q(x)⟩. x∈⋃τ⇩1} ∈ Cont(τ⇩1,τ⇩3)"
shows "{⟨x,⟨p(x),q(x)⟩⟩. x∈⋃τ⇩1} ∈ Cont(τ⇩1,τ⇩2×⇩tτ⇩3)"
proof -
let ?X = "⋃τ⇩1"
let ?Y = "⋃τ⇩2"
let ?Z = "⋃τ⇩3"
let ?f = "{⟨x,p(x)⟩. x∈?X}"
let ?g = "{⟨x,q(x)⟩. x∈?X}"
let ?h = "{⟨x,⟨p(x),q(x)⟩⟩. x∈?X}"
from assms(4,5) have "?f:?X→?Y" and "?g:?X→?Z" unfolding Cont_def
by auto
with assms(2,3) have hFun: "?h:?X→⋃(τ⇩2×⇩tτ⇩3)"
using prod_fun_val(1) using Top_1_4_T1(3) by simp
moreover have "IsContinuous(τ⇩1,τ⇩2×⇩tτ⇩3,?h)"
proof -
let ?B = "ProductCollection(τ⇩2,τ⇩3)"
from assms(1,2,3) hFun have "two_top_spaces0(τ⇩1,τ⇩2×⇩tτ⇩3,?h)"
using Top_1_4_T1(1) unfolding two_top_spaces0_def by simp
moreover from assms(2,3) have "?B {is a base for} (τ⇩2×⇩tτ⇩3)"
using Top_1_4_T1(2) by simp
moreover have "∀W∈?B. ?h-(W) ∈ τ⇩1"
proof -
{ fix W assume "W∈?B"
then obtain U V where "U∈τ⇩2" "V∈τ⇩3" "W=U×V"
unfolding ProductCollection_def by auto
have "∀x∈?X. ⟨p(x),q(x)⟩ = ⟨?f(x),?g(x)⟩"
proof -
{ fix x assume "x∈?X"
then have "⟨p(x),q(x)⟩ = ⟨?f(x),?g(x)⟩"
using ZF_fun_from_tot_val1 by simp
} thus ?thesis by auto
qed
then have "?h = {⟨x,⟨?f(x),?g(x)⟩⟩. x∈?X}" by (rule set_comp_eq)
with assms(1,4,5) ‹?f:?X→?Y› ‹?g:?X→?Z› ‹U∈τ⇩2› ‹V∈τ⇩3› ‹W=U×V›
have "?h-(W) ∈ τ⇩1" using vimage_prod(3)
unfolding Cont_def IsContinuous_def IsATopology_def by auto
} thus ?thesis by simp
qed
ultimately show ?thesis by (rule two_top_spaces0.Top_ZF_2_1_L5)
qed
ultimately show ?thesis unfolding Cont_def by simp
qed

text‹Two continuous functions into a Hausdorff space are equal on a closed set.
Note that in the lemma below $f$ is assumed to map $X_1$ to $X_2$ in the locale, we only
need to add a similar assumption for the second function. ›

lemma (in two_top_spaces0) two_fun_eq_closed:
assumes "g:X⇩1→X⇩2" "f {is continuous}" "g {is continuous}"  "τ⇩2 {is T⇩2}"
shows "{x∈X⇩1. f(x)=g(x)} {is closed in} τ⇩1"
proof -
let ?D = "{x∈X⇩1. f(x)=g(x)}"
let ?h = "{⟨x,⟨f(x),g(x)⟩⟩. x∈X⇩1}"
have "?h-({⟨y,y⟩. y∈X⇩2}) {is closed in} τ⇩1"
proof -
have "two_top_spaces0(τ⇩1,ProductTopology(τ⇩2,τ⇩2),?h)"
proof
from tau1_is_top tau2_is_top
show "τ⇩1 {is a topology}" and "ProductTopology(τ⇩2,τ⇩2) {is a topology}"
using Top_1_4_T1(1) by auto
from tau1_is_top tau2_is_top fmapAssum assms(1)
show "?h : ⋃τ⇩1 → ⋃ProductTopology(τ⇩2, τ⇩2)"
using vimage_prod(1) Top_1_4_T1(3) by simp
qed
moreover
have "IsContinuous(τ⇩1,ProductTopology(τ⇩2,τ⇩2),?h)"
proof -
from tau1_is_top tau2_is_top have "prod_top_spaces0(τ⇩1,τ⇩2,τ⇩2)"
unfolding prod_top_spaces0_def by simp
with fmapAssum assms(1,2,3) show ?thesis
using prod_top_spaces0.cont_funcs_prod by simp
qed
moreover
from tau2_is_top assms(4)
have "{⟨y,y⟩. y∈X⇩2} {is closed in} ProductTopology(τ⇩2,τ⇩2)"
using t2_iff_diag_closed by simp
ultimately show ?thesis using two_top_spaces0.TopZF_2_1_L1
by simp
qed
with fmapAssum assms(1) show ?thesis using vimage_prod(4)
by simp
qed

text‹Closure of an image of a singleton by a relation in $X\times Y$ is contained in the
image of this singleton by the closure of the relation (in the product topology).
Compare the proof of Metamath's theorem with the same name.›

lemma imasncls:
assumes "T {is a topology}"  "S {is a topology}" "R ⊆ (⋃T)×(⋃S)" "x∈⋃T"
shows "Closure(R{x},S) ⊆ Closure(R,T×⇩tS){x}"
proof -
let ?X = "⋃T"
let ?Y = "⋃S"
let ?f = "{⟨y,⟨x,y⟩⟩. y∈?Y}"
from assms(3) have "R{x} = ?f-(R)" by blast
hence "Closure(R{x},S) = Closure(?f-(R),S)" by simp
also have "Closure(?f-(R),S) ⊆ ?f-(Closure(R,T×⇩tS))"
proof -
from assms(1,2,4) have "?f ∈ Cont(S,T×⇩tS)"
using const_cont_sp id_cont_sp cont_funcs_prod1 by simp
with assms(1,2,3) have
"two_top_spaces0(S,T×⇩tS,?f)" "IsContinuous(S,T×⇩tS,?f)" "R ⊆ ⋃(T×⇩tS)"
unfolding Cont_def two_top_spaces0_def using Top_1_4_T1(1,3)
by auto
then show "Closure(?f-(R),S) ⊆ ?f-(Closure(R,T×⇩tS))"
using two_top_spaces0.im_cl_in_cl_im by simp
qed
also
have "Closure(R,T×⇩tS) ⊆ ?X×?Y"
proof -
from assms(1,2,3) have "topology0(T×⇩tS)" "R ⊆ ⋃(T×⇩tS)"
unfolding topology0_def using Top_1_4_T1(1,3) by auto
then have "Closure(R,T×⇩tS) ⊆ ⋃(T×⇩tS)" by (rule topology0.Top_3_L11)
with assms(1,2) show ?thesis using Top_1_4_T1(3) by simp
qed
with assms(4) have "?f-(Closure(R,T×⇩tS)) = Closure(R,T×⇩tS){x}" by blast
finally show "Closure(R{x},S) ⊆ Closure(R,T×⇩tS){x}" by simp
qed

subsection‹Pasting lemma›

text‹The classical pasting lemma states that if $U_1,U_2$ are both open (or closed) and a function
is continuous when restricted to both $U_1$ and $U_2$ then it is continuous
when restricted to $U_1 \cup U_2$. In this section we prove a generalization statement
stating that the set $\{ U \in \tau_1 | f|_U$ is continuous $\}$ is a
topology.›

text‹A typical statement of the pasting lemma uses the notion of a function
restricted to a set being continuous without specifying the topologies with
respect to which this continuity holds.
In ‹two_top_spaces0› context the notation ‹g {is continuous}›
means continuity wth respect to topologies $\tau_1, \tau_2$.
The next lemma is a special case of ‹partial_fun_cont› and states that if
for some set $A\subseteq X_1=\bigcup \tau_1$
the function $f|_A$ is continuous (with respect to $(\tau_1, \tau_2)$), then
$A$ has to be open. This clears up terminology and indicates why we need
to pay attention to the issue of which topologies we talk about when we say
that the restricted (to some closed set for example) function is continuos.
›

lemma (in two_top_spaces0) restriction_continuous1:
assumes A1: "A ⊆ X⇩1" and A2: "restrict(f,A) {is continuous}"
shows "A ∈ τ⇩1"
proof -
from assms have "two_top_spaces1(τ⇩1,τ⇩2)" and
"restrict(f,A):A→X⇩2" and "restrict(f,A) {is continuous}"
using tau1_is_top tau2_is_top two_top_spaces1_def fmapAssum restrict_fun
by auto
then show ?thesis using two_top_spaces1.partial_fun_cont by simp
qed

text‹If a fuction is continuous on each set of a collection of open sets, then
it is continuous on the union of them. We could use continuity with respect to
the relative topology here, but we know that on open sets this is the same as the
original topology.›

lemma (in two_top_spaces0) pasting_lemma1:
assumes A1: "M ⊆ τ⇩1" and A2: "∀U∈M. restrict(f,U)  {is continuous}"
shows "restrict(f,⋃M) {is continuous}"
proof -
{ fix V assume "V∈τ⇩2"
from A1 have "⋃M ⊆ X⇩1" by auto
then have "restrict(f,⋃M)-(V) = f-(V) ∩ (⋃M)"
using func1_2_L1 fmapAssum by simp
also have "… = ⋃ {f-(V) ∩ U. U∈M}" by auto
finally have "restrict(f,⋃M)-(V) = ⋃ {f-(V) ∩ U. U∈M}" by simp
moreover
have "{f-(V) ∩ U. U∈M} ∈ Pow(τ⇩1)"
proof -
{ fix W assume "W ∈ {f-(V) ∩ U. U∈M}"
then obtain U where "U∈M" and I: "W = f-(V) ∩ U" by auto
with A2 have "restrict(f,U) {is continuous}" by simp
with ‹V∈τ⇩2› have "restrict(f,U)-(V) ∈ τ⇩1"
using IsContinuous_def by simp
moreover from ‹⋃M ⊆ X⇩1› and ‹U∈M›
have "restrict(f,U)-(V) = f-(V) ∩ U"
using fmapAssum func1_2_L1 by blast
ultimately have "f-(V) ∩ U ∈ τ⇩1" by simp
with I have "W ∈ τ⇩1" by simp
} then show ?thesis by auto
qed
then have  "⋃{f-(V) ∩ U. U∈M} ∈ τ⇩1"
using tau1_is_top IsATopology_def by auto
ultimately have "restrict(f,⋃M)-(V) ∈ τ⇩1"
by simp
} then show ?thesis using IsContinuous_def by simp
qed

text‹If a function is continuous on two sets, then it is continuous
on intersection.›

lemma (in two_top_spaces0) cont_inter_cont:
assumes A1: "A ⊆ X⇩1" "B ⊆ X⇩1" and
A2: "restrict(f,A)  {is continuous}"  "restrict(f,B)  {is continuous}"
shows "restrict(f,A∩B)  {is continuous}"
proof -
{ fix V assume "V∈τ⇩2"
with assms have
"restrict(f,A)-(V) = f-(V) ∩ A"  "restrict(f,B)-(V) = f-(V) ∩ B" and
"restrict(f,A)-(V) ∈ τ⇩1" and "restrict(f,B)-(V) ∈ τ⇩1"
using func1_2_L1 fmapAssum IsContinuous_def by auto
then have "(restrict(f,A)-(V)) ∩ (restrict(f,B)-(V)) = f-(V) ∩ (A∩B)"
by auto
moreover
from A2 ‹V∈τ⇩2› have
"restrict(f,A)-(V) ∈ τ⇩1" and "restrict(f,B)-(V) ∈ τ⇩1"
using IsContinuous_def by auto
then have "(restrict(f,A)-(V)) ∩ (restrict(f,B)-(V)) ∈ τ⇩1"
using tau1_is_top IsATopology_def by simp
moreover
from A1 have "(A∩B) ⊆ X⇩1" by auto
then have "restrict(f,A∩B)-(V) = f-(V) ∩ (A∩B)"
using func1_2_L1 fmapAssum by simp
ultimately have "restrict(f,A∩B)-(V) ∈ τ⇩1" by simp
} then show ?thesis using  IsContinuous_def by auto
qed

text‹The collection of open sets $U$ such that $f$ restricted to
$U$ is continuous, is a topology.›

theorem (in two_top_spaces0) pasting_theorem:
shows "{U ∈ τ⇩1. restrict(f,U) {is continuous}} {is a topology}"
proof -
let ?T = "{U ∈ τ⇩1. restrict(f,U) {is continuous}}"
have "∀M∈Pow(?T). ⋃M ∈ ?T"
proof
fix M assume "M ∈ Pow(?T)"
then have "restrict(f,⋃M) {is continuous}"
using pasting_lemma1 by auto
with ‹M ∈ Pow(?T)› show "⋃M ∈ ?T"
using tau1_is_top IsATopology_def by auto
qed
moreover have "∀U∈?T.∀V∈?T. U∩V ∈ ?T"
using cont_inter_cont tau1_is_top IsATopology_def by auto
ultimately show ?thesis using IsATopology_def by simp
qed

text‹0 is continuous.›

corollary (in two_top_spaces0) zero_continuous: shows "0 {is continuous}"
proof -
let ?T = "{U ∈ τ⇩1. restrict(f,U) {is continuous}}"
have "?T {is a topology}" by (rule pasting_theorem)
then have "0∈?T" by (rule empty_open)
hence "restrict(f,0) {is continuous}" by simp
moreover have "restrict(f,0) = 0" by simp
ultimately show ?thesis by simp
qed

end
`