Up to index of Isabelle/ZF/IsarMathLib
theory Topology_ZF_2(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005, 2006 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. *) header {*\isaheader{Topology\_ZF\_2.thy}*} theory Topology_ZF_2 imports Topology_ZF_1 func1 Fol1 begin section{*Continuous functions.*} 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. Recall that in Isabelle/ZF @{text "f-``(A)"} denotes the inverse image of (set) $A$ with respect to (function) $f$. *} constdefs "IsContinuous(τ1,τ2,f) ≡ (∀U∈τ2. f-``(U) ∈ τ1)" 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 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 "cl1(A)"} and @{text "cl2(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 X1 defines X1_def [simp]: "X1 ≡ \<Union>τ1" fixes X2 defines X2_def [simp]: "X2 ≡ \<Union>τ2" fixes f assumes fmapAssum: "f: X1 -> X2" fixes isContinuous ("_ {is continuous}" [50] 50) defines isContinuous_def [simp]: "g {is continuous} ≡ IsContinuous(τ1,τ2,g)" fixes cl1 defines cl1_def [simp]: "cl1(A) ≡ Closure(A,τ1)" fixes cl2 defines cl2_def [simp]: "cl2(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) ⊆ X1" using func1_1_L3 by simp; moreover from fmapAssum have "f-``(X2 - D) = X1 - f-``(D)" using Pi_iff function_vimage_Diff func1_1_L4 by auto; ultimately have "X1 - f-``(X2 - D) = f-``(D)" by auto; moreover from A1 A2 have "(X1 - f-``(X2 - 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 ⊆ X1" shows "f``(cl1(A)) ⊆ cl2(f``(A))" proof - from fmapAssum have "f``(A) ⊆ cl2(f``(A))" using func1_1_L6 topol_cntxs_valid topology0.Top_3_L10 by simp; with fmapAssum have "f-``(f``(A)) ⊆ f-``(cl2(f``(A)))" using func1_1_L7 by auto; moreover from fmapAssum A2 have "A ⊆ f-``(f``(A))" using func1_1_L9 by simp; ultimately have "A ⊆ f-``(cl2(f``(A)))" by auto; with fmapAssum A1 have "f``(cl1(A)) ⊆ f``(f-``(cl2(f``(A))))" using func1_1_L6 func1_1_L8 IsClosed_def topol_cntxs_valid topology0.Top_3_L7 topology0.Top_3_L13 by simp; moreover from fmapAssum have "f``(f-``(cl2(f``(A)))) ⊆ cl2(f``(A))" using fun_is_function function_image_vimage by simp; ultimately show "f``(cl1(A)) ⊆ cl2(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 ⊆ X1 --> f``(cl1(A)) ⊆ cl2(f``(A)))" shows "∀B. ( B ⊆ X2 --> cl1(f-``(B)) ⊆ f-``(cl2(B)) )" proof - { fix B assume A2: "B ⊆ X2"; from fmapAssum A1 have "f``(cl1(f-``(B))) ⊆ cl2(f``(f-``(B)))" using func1_1_L3 by simp; moreover from fmapAssum A2 have "cl2(f``(f-``(B))) ⊆ cl2(B)" using fun_is_function function_image_vimage func1_1_L6 topol_cntxs_valid topology0.top_closure_mono by simp; ultimately have "f-``(f``(cl1(f-``(B)))) ⊆ f-``(cl2(B))" using fmapAssum fun_is_function func1_1_L7 by auto; moreover from fmapAssum A2 have "cl1(f-``(B)) ⊆ f-``(f``(cl1(f-``(B))))" using func1_1_L3 func1_1_L9 IsClosed_def topol_cntxs_valid topology0.Top_3_L7 by simp; ultimately have "cl1(f-``(B)) ⊆ f-``(cl2(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 showing equavalence of four definitions of continuity.*} lemma (in two_top_spaces0) Top_ZF_2_1_L4: assumes A1: "∀B. ( B ⊆ X2 --> cl1(f-``(B)) ⊆ f-``(cl2(B)) )" shows "f {is continuous}" proof - { fix U assume A2: "U ∈ τ2" from A2 have "(X2 - U) {is closed in} τ2" using topol_cntxs_valid topology0.Top_3_L9 by simp; moreover have "X2 - U ⊆ \<Union>τ2" by auto; ultimately have "cl2(X2 - U) = X2 - U" using topol_cntxs_valid topology0.Top_3_L8 by simp; moreover from A1 have "cl1(f-``(X2 - U)) ⊆ f-``(cl2(X2 - U))" by auto; ultimately have "cl1(f-``(X2 - U)) ⊆ f-``(X2 - U)" by simp; moreover from fmapAssum have "f-``(X2 - U) ⊆ cl1(f-``(X2 - U))" using func1_1_L3 topol_cntxs_valid topology0.Top_3_L10 by simp; ultimately have "f-``(X2 - 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{*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 D1: "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 D1 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 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 = "{\<Inter>A. A ∈ Fin(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 A3: "U∈?C" { assume "f-``(U)=0" with tau1_is_top have "f-``(U) ∈ τ1" using IsATopology_def by simp;} moreover { assume A4: "f-``(U)≠0" then have "U≠0" by (rule func1_1_L13); moreover from A3 obtain A where D1:"A ∈ Fin(B)" and D2: "U = \<Inter>A" by auto; ultimately have "\<Inter>A≠0" by simp; hence I: "A≠0" by (rule Finite1_L9); then have "{f-``(W). W∈A} ≠ 0" by simp; moreover from A2 D1 have "{f-``(W). W∈A} ∈ Fin(τ1)" by (rule Finite1_L6); ultimately have "\<Inter>{f-``(W). W∈A} ∈ τ1" using topol_cntxs_valid topology0.Top_1_L3 by simp; moreover from A1 D1 have "A ⊆ τ2" using FinD IsAsubBaseFor_def by auto; with tau2_is_top have "A ⊆ Pow(X2)" using IsATopology_def by auto; with fmapAssum I have "f-``(\<Inter>A) = \<Inter>{f-``(W). W∈A}" using func1_1_L12 by simp; with D2 have "f-``(U) = \<Inter>{f-``(W). W∈A}" 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; end
lemma topol_cntxs_valid(1):
two_top_spaces0(τ1, τ2, f) ==> topology0(τ1)
and topol_cntxs_valid(2):
two_top_spaces0(τ1, τ2, f) ==> topology0(τ2)
lemma TopZF_2_1_L1:
[| two_top_spaces0(τ1, τ2, f); IsContinuous(τ1, τ2, f); D {is closed in} τ2 |] ==> f -`` D {is closed in} τ1
lemma Top_ZF_2_1_L2:
[| two_top_spaces0(τ1, τ2, f); ∀D. D {is closed in} τ2 --> f -`` D {is closed in} τ1; A ⊆ \<Union>τ1 |] ==> f `` Closure(A, τ1) ⊆ Closure(f `` A, τ2)
lemma Top_ZF_2_1_L3:
[| two_top_spaces0(τ1, τ2, f); ∀A. A ⊆ \<Union>τ1 --> f `` Closure(A, τ1) ⊆ Closure(f `` A, τ2) |] ==> ∀B. B ⊆ \<Union>τ2 --> Closure(f -`` B, τ1) ⊆ f -`` Closure(B, τ2)
lemma Top_ZF_2_1_L4:
[| two_top_spaces0(τ1, τ2, f); ∀B. B ⊆ \<Union>τ2 --> Closure(f -`` B, τ1) ⊆ f -`` Closure(B, τ2) |] ==> IsContinuous(τ1, τ2, f)
lemma Top_ZF_2_1_L5:
[| two_top_spaces0(τ1, τ2, f); B {is a base for} τ2; ∀U∈B. f -`` U ∈ τ1 |] ==> IsContinuous(τ1, τ2, f)
lemma Top_ZF_2_1_L6:
[| two_top_spaces0(τ1, τ2, f); B {is a subbase for} τ2; ∀U∈B. f -`` U ∈ τ1 |] ==> IsContinuous(τ1, τ2, f)