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