# Theory Topology_ZF_2

theory Topology_ZF_2
imports Topology_ZF_1 func1
(*     This file is a part of IsarMathLib -     a library of formalized mathematics for Isabelle/Isar.    Copyright (C) 2005 - 2008  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 APARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOTLIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS ORBUSINESS 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 THEUSE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.*)header{*\isaheader{Topology\_ZF\_2.thy}*}theory Topology_ZF_2 imports Topology_ZF_1 func1 Fol1begintext{*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. *}section{*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 contiuous 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 @{text "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{*A trivial example of a continuous function - identity is continuous.*}lemma id_cont: shows "IsContinuous(τ,τ,id(\<Union>τ))"proof -  { fix U assume "U∈τ"    then have "id(\<Union>τ)-(U) = U" using vimage_id_same by auto    with U∈τ have "id(\<Union>τ)-(U) ∈ τ" by simp  } then show "IsContinuous(τ,τ,id(\<Union>τ))" using IsContinuous_def    by simpqedtext{*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 @{text "cl⇩1(A)"} and  @{text "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 ≡ \<Union>τ⇩1"    fixes X⇩2  defines X2_def [simp]: "X⇩2 ≡ \<Union>τ⇩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 @{text "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 simpqedtext{*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 autoqed    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 simpqed;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  @{text " Top_ZF_2_1_L1"},   @{text " Top_ZF_2_1_L2"} and @{text " 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 ⊆ \<Union>τ⇩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 simpqed;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 = \<Union>A"      using IsAbaseFor_def by auto    with A2 have "{f-(U). U∈A} ⊆ τ⇩1" by auto    with tau1_is_top have "\<Union> {f-(U). U∈A} ∈ τ⇩1"      using IsATopology_def by simp    moreover from A ⊆ B V = \<Union>A have "f-(V) = \<Union>{f-(U). U∈A}"       by auto;    ultimately have "f-(V) ∈  τ⇩1" by simp  } then show "f {is continuous}" using IsContinuous_def    by simpqed;  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 = "{\<Inter>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 = \<Inter>A" 	by auto      ultimately have "\<Inter>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 "\<Inter>{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 = \<Inter>A have "f-(U) = \<Inter>{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 simpqedtext{*A dual of @{text " 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: "\<B> {is a base for} τ⇩1" and A2: "∀B∈\<B>. f(B) ∈ τ⇩2" and A3: "U∈τ⇩1"   shows "f(U) ∈ τ⇩2"proof -  from A1 A3 obtain \<E> where "\<E> ∈ Pow(\<B>)" and "U = \<Union>\<E>" using Top_1_2_L1 by blast  with A1 have "f(U) = \<Union>{f(E). E ∈ \<E>}" using Top_1_2_L5  fmapAssum image_of_Union    by auto  moreover   from A2 \<E> ∈ Pow(\<B>) have "{f(E). E ∈ \<E>} ∈ Pow(τ⇩2)" by auto  then have "\<Union>{f(E). E ∈ \<E>} ∈ τ⇩2" using tau2_is_top IsATopology_def by simp  ultimately show ?thesis using tau2_is_top IsATopology_def by autoqedtext{*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 simptext{*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 simpsection{*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(\<Union>T,\<Union>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 autotext{*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 simptext{*A continuous bijection that is an open map is a homeomorphism.*}lemma bij_cont_open_homeo:   assumes "f ∈ bij(\<Union>T,\<Union>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 autotext{*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: "\<B> {is a base for} τ⇩1"  and A3: "\<C> {is a base for} τ⇩2" and  A4: "∀U∈\<C>. f-(U) ∈ τ⇩1" and A5: "∀V∈\<B>. 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: "\<B> {is a base for} τ⇩1" and   A3: "{f(B). 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∈\<B>}"      then obtain B where "B∈\<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∈\<B> I have "f-(C) ∈ τ⇩1"          using bij_def inj_vimage_image base_sets_open by auto    } hence "∀C ∈ {f(B). B∈\<B>}. f-(C) ∈ τ⇩1" by auto    with A3 show ?thesis by (rule Top_ZF_2_1_L5)  qed  moreover   from A3 have "∀B∈\<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 simpqedtext{*Interior is a topological invariant.*}theorem int_top_invariant: assumes A1: "A⊆\<Union>T" and A2: "IsAhomeomorphism(T,S,f)"  shows "f(Interior(A,T)) = Interior(f(A),S)"proof -  let ?\<A> = "{U∈T. U⊆A}"  have I: "{f(U). U∈?\<A>} = {V∈S. V ⊆ f(A)}"  proof    from A2 show "{f(U). U∈?\<A>} ⊆ {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 ⊆ \<Union>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∈?\<A>}" by auto    } thus "{V∈S. V ⊆ f(A)} ⊆ {f(U). U∈?\<A>}" by auto  qed  have "f(Interior(A,T)) =  f(\<Union>?\<A>)" unfolding Interior_def by simp  also from A2 have "… = \<Union>{f(U). U∈?\<A>}"     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 simpqedsection{*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(\<Union>T,Y)"  shows   "{f(U). U∈T} {is a topology}" and  "{ {f(x).x∈U}. U∈T} {is a topology}" and   "(\<Union>{f(U). U∈T}) = Y" and   "IsAhomeomorphism(T, {f(U). U∈T},f)"proof -  from A2 have "f ∈ inj(\<Union>T,Y)" using bij_def by simp   then have "f:\<Union>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(\<Union>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 "(\<Union>?M⇩T) ∈ T" using IsATopology_def by simp    hence "f(\<Union>?M⇩T) ∈  ?S" by auto     moreover have "f(\<Union>?M⇩T) = \<Union>M"    proof -      from f:\<Union>T->Y ?M⇩T ⊆ T  have "f(\<Union>?M⇩T) = \<Union>{f(U). U∈?M⇩T}"         using image_of_Union by auto       moreover have "{f(U). U∈?M⇩T} = M"      proof -        from f:\<Union>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(\<Union>?M⇩T) = \<Union>M" by simp     qed    ultimately have "\<Union>M ∈ ?S" by auto  } then have "∀M∈Pow(?S). \<Union>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 ⊆ \<Union>T"  "V⇩T ⊆ \<Union>T"        using bij_def by auto      with f ∈ inj(\<Union>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:\<Union>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 "\<Union>?S =  Y"  proof     from f:\<Union>T->Y have "∀U∈T. f(U) ⊆ Y" using func1_1_L6 by simp    thus "\<Union>?S ⊆ Y" by auto    from A1 have "f(\<Union>T) ⊆ \<Union>?S" using IsATopology_def by auto     with A2 show "Y ⊆ \<Union>?S" using bij_def surj_range_image_domain       by auto  qed  show "IsAhomeomorphism(T,?S,f)"  proof -    from A2  \<Union>?S =  Y have "f ∈ bij(\<Union>T,\<Union>?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 ⊆ \<Union>T" and "f-(V) = f-(f(U))"  by auto        with f ∈ inj(\<Union>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   qedqedsection{*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 twonatural possibilities for the pairs of topologies with respect to which this function maybe continuous. One is obvously the original $\tau_1,\tau_2$ and in the second onethe first element of the pair is the topology relative to the domain of thefunction: $\{A\cap U | U \in \tau_1\}$. These two possibilities are not exactlythe 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;qedtext{*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 @{text "restr_cont"} and @{text "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 "\<Union>τ⇩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 \<Union>τ⇩3 = A have "g: \<Union>τ⇩3 -> \<Union>τ⇩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(\<Union>τ⇩3),g)"    by (rule two_top_spaces0.restr_image_cont);  moreover note \<Union>τ⇩3 = A  ultimately show ?thesis by simp;qedtext{*We need a context similar to @{text "two_top_spaces0"} but withoutthe 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 ≡ \<Union>τ⇩1"  fixes X⇩2  defines X2_def [simp]: "X⇩2 ≡ \<Union>τ⇩2"text{*If a partial function $g:X_1\supseteq A\rightarrow X_2$ is continuous withrespect 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 simpqedtext{*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 simpqedsection{*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 studythe properties of $f$ with respect to the product topology $\tau_1\times \tau_2$and $\tau_3$. This situation is similar as in locale @{text "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 ≡ \<Union>τ⇩1"  fixes X⇩2  defines X2_def [simp]: "X⇩2 ≡ \<Union>τ⇩2"  fixes X⇩3  defines X3_def [simp]: "X⇩3 ≡ \<Union>τ⇩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 simptext{*Fixing the second variable in a two-variable continuous function results in acontinuous 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 simptext{*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:\<Union>τ⇩1->\<Union>η⇩1"  and A3b: "f⇩2:\<Union>τ⇩2->\<Union>η⇩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 ∈ \<Union>τ⇩1×\<Union>τ⇩2}"  shows "IsContinuous(ProductTopology(τ⇩1,τ⇩2),ProductTopology(η⇩1,η⇩2),g)"proof -  let ?τ = "ProductTopology(τ⇩1,τ⇩2)"  let ?η = "ProductTopology(η⇩1,η⇩2)"  let ?X⇩1 = "\<Union>τ⇩1"  let ?X⇩2 = "\<Union>τ⇩2"  let ?Y⇩1 = "\<Union>η⇩1"  let ?Y⇩2 = "\<Union>η⇩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))⟩ ∈ \<Union>η⇩1×\<Union>η⇩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 "\<Union>?τ = ?X⇩1×?X⇩2" and "\<Union>?η = ?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 simpqedtext{*A reformulation of the @{text "cart_prod_cont"} lemma above in slightly different notation.*}theorem (in two_top_spaces0) product_cont_functions:  assumes "f:X⇩1->X⇩2" "g:\<Union>τ⇩3->\<Union>τ⇩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×\<Union>τ⇩3})"proof -  have "{⟨⟨x,y⟩,⟨fx,gy⟩⟩. ⟨x,y⟩∈X⇩1×\<Union>τ⇩3} = {⟨p,⟨f(fst(p)),g(snd(p))⟩⟩. p ∈ X⇩1×\<Union>τ⇩3}"    by force  with tau1_is_top tau2_is_top assms show ?thesis using cart_prod_cont by simpqedtext{*A special case of @{text "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:\<Union>τ⇩1->\<Union>η⇩1" and A4: "IsContinuous(τ⇩1,η⇩1,f⇩1)" and  A5: "g = {⟨p, ⟨f⇩1(fst(p)),snd(p)⟩⟩. p ∈ \<Union>τ⇩1×\<Union>τ⇩2}"  shows "IsContinuous(ProductTopology(τ⇩1,τ⇩2),ProductTopology(η⇩1,τ⇩2),g)"proof -  let ?f⇩2 = "id(\<Union>τ⇩2)"  have "∀x∈\<Union>τ⇩2. ?f⇩2(x) = x" using id_conv by blast  hence I: "∀p ∈ \<Union>τ⇩1×\<Union>τ⇩2. snd(p) = ?f⇩2(snd(p))" by simp  note A1 A1a A2 A1a A3  moreover have "?f⇩2:\<Union>τ⇩2->\<Union>τ⇩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 ∈ \<Union>τ⇩1×\<Union>τ⇩2}"  proof    from A5 I show  "g ⊆ {⟨p, ⟨f⇩1(fst(p)),?f⇩2(snd(p))⟩⟩. p ∈ \<Union>τ⇩1×\<Union>τ⇩2}"      by auto    from A5 I show "{⟨p, ⟨f⇩1(fst(p)),?f⇩2(snd(p))⟩⟩. p ∈ \<Union>τ⇩1×\<Union>τ⇩2} ⊆ g"      by auto  qed  ultimately show ?thesis by (rule cart_prod_cont)qed section{*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 statementstating that the set $\{ U \in \tau_1 | f|_U$ is continuous $\}$ is atopology. *}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 @{text "two_top_spaces0"} context the notation @{text "g {is continuous}"}means continuity wth respect to topologies $\tau_1, \tau_2$.The next lemma is a special case of @{text "partial_fun_cont"} and states that iffor 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 needto pay attention to the issue of which topologies we talk about when we saythat 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 simpqedtext{*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,\<Union>M) {is continuous}"proof -  { fix V assume "V∈τ⇩2"    from A1 have "\<Union>M ⊆ X⇩1" by auto    then have "restrict(f,\<Union>M)-(V) = f-(V) ∩ (\<Union>M)"      using func1_2_L1 fmapAssum by simp    also have "… = \<Union> {f-(V) ∩ U. U∈M}" by auto    finally have "restrict(f,\<Union>M)-(V) = \<Union> {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 \<Union>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  "\<Union>{f-(V) ∩ U. U∈M} ∈ τ⇩1"       using tau1_is_top IsATopology_def by auto    ultimately have "restrict(f,\<Union>M)-(V) ∈ τ⇩1"      by simp  } then show ?thesis using IsContinuous_def by simpqedtext{*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 autoqedtext{*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). \<Union>M ∈ ?T"   proof    fix M assume "M ∈ Pow(?T)"    then have "restrict(f,\<Union>M) {is continuous}"      using pasting_lemma1 by auto    with M ∈ Pow(?T) show "\<Union>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 simpqedtext{*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 simpqedend