Theory Topology_ZF_6

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

    Copyright (C) 2012-2013 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section ‹Topology 6›

theory Topology_ZF_6 imports Topology_ZF_4 Topology_ZF_2 Topology_ZF_1

begin

text‹
  This theory deals with the relations between continuous functions and convergence
  of filters. At the end of the file there some results about the building of functions
  in cartesian products.
›

subsection‹Image filter›

text‹First of all, we will define the appropriate tools to work with functions
and filters together.›

text‹We define the image filter as the collections of supersets of of images of sets from a filter.
›

definition
  ImageFilter ("_[_].._" 98)
  where "𝔉 {is a filter on} X ⟹ f:X→Y ⟹ f[𝔉]..Y ≡ {A∈Pow(Y). ∃D∈{f``(B) .B∈𝔉}. D⊆A}"

text‹Note that in the previous definition, it is necessary to state
 $Y$ as the final set because $f$ is also a function to every superset of its range.
$X$ can be changed by ‹domain(f)› without any change in the definition.›

lemma base_image_filter:
  assumes "𝔉 {is a filter on} X" "f:X→Y"
  shows "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..Y)" and "(f[𝔉]..Y) {is a filter on} Y"
proof-
  {
    assume "0 ∈ {f``B .B∈𝔉}"
    then obtain B where "B∈𝔉" and f_B:"f``B=0" by auto
    then have "B∈Pow(X)" using assms(1) IsFilter_def by auto
    then have "f``B={f`b. b∈B}" using image_fun assms(2) by auto
    with f_B have "{f`b. b∈B}=0" by auto
    then have "B=0" by auto
    with ‹B∈𝔉› have "False" using IsFilter_def assms(1) by auto
  }
  then have "0∉{f``B .B∈𝔉}" by auto
  moreover
  from assms(1) obtain S where "S∈𝔉" using IsFilter_def by auto
  then have "f``S∈{f``B .B∈𝔉}" by auto
  then have nA:"{f``B .B∈𝔉}≠0" by auto
  moreover
  {
    fix A B
    assume "A∈{f``B .B∈𝔉}" and "B∈{f``B .B∈𝔉}"
    then obtain AB BB where "A=f``AB" "B=f``BB" "AB∈𝔉" "BB∈𝔉" by auto
    then have "A∩B=(f``AB)∩(f``BB)" by auto
    then have I: "f``(AB∩BB)⊆A∩B" by auto
    moreover
    from assms(1) I ‹AB∈𝔉›‹BB∈𝔉› have "AB∩BB∈𝔉" using IsFilter_def by auto
    ultimately have "∃D∈{f``B .B∈𝔉}. D⊆A∩B" by auto
  }
  then have "∀A∈{f``B .B∈𝔉}. ∀B∈{f``B .B∈𝔉}. ∃D∈{f``B .B∈𝔉}. D⊆A∩B" by auto
  ultimately have sbc:"{f``B .B∈𝔉} {satisfies the filter base condition}" 
    using SatisfiesFilterBase_def by auto
  moreover
  {
    fix t
    assume "t∈{f``B . B∈𝔉}"
    then obtain B where "B∈𝔉" and im_def:"f``B=t" by auto
    with assms(1) have "B∈Pow(X)" unfolding IsFilter_def by auto
    with im_def assms(2) have "t={f`x. x∈B}" using image_fun by auto
    with assms(2) ‹B∈Pow(X)› have "t⊆Y" using apply_funtype by auto
    }
  then have nB:"{f``B . B∈𝔉}⊆Pow(Y)" by auto
  ultimately
  have "(({f``B .B∈𝔉} {is a base filter} {A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}) ∧ (⋃{A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}=Y))" using base_unique_filter_set2 
    by force
  then have "{f``B .B∈𝔉} {is a base filter} {A ∈ Pow(Y) . ∃D∈{f``B .B∈𝔉}. D ⊆ A}" by auto
  with assms show "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..Y)" using ImageFilter_def  by auto
  moreover
  note sbc
  moreover
  {
    from nA obtain D where I: "D∈{f``B .B∈𝔉}" by blast
    moreover from I nB have "D⊆Y" by auto
    ultimately have "Y∈{A∈Pow(Y). ∃D∈{f``B .B∈𝔉}. D⊆A}" by auto
  }
  then have "⋃{A∈Pow(Y). ∃D∈{f``B .B∈𝔉}. D⊆A}=Y" by auto
  ultimately show "(f[𝔉]..Y) {is a filter on} Y" using basic_filter
    ImageFilter_def assms by auto 
qed

subsection‹Continuous at a point vs. globally continuous›

text‹In this section we show that continuity of a function implies local continuity (at a point)
  and that local continuity at all points implies (global) continuity.›

text‹If a function is continuous, then it is continuous at every point.›

lemma cont_global_imp_continuous_x:
  assumes "x∈⋃τ⇩1" "IsContinuous(τ⇩1,τ⇩2,f)" "f:(⋃τ⇩1)→(⋃τ⇩2)" "x∈⋃τ⇩1"
  shows "∀U∈τ⇩2. f`(x)∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``(V)⊆U)"
proof-
  {
    fix U
    assume AS:"U∈τ⇩2" "f`(x)∈U"
    then have "f-``(U)∈τ⇩1" using assms(2) IsContinuous_def by auto
    moreover
    from assms(3) have "f``(f-``(U))⊆U" using function_image_vimage fun_is_fun 
      by auto
    moreover
    from assms(3) assms(4) AS(2) have "x∈f-``(U)" using func1_1_L15 by auto
    ultimately have "∃V∈τ⇩1. x∈V ∧ f``V⊆U" by auto
  }
  then show "∀U∈τ⇩2. f`(x)∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``(V)⊆U)" by auto
qed

text‹A function that is continuous at every point of its domain is continuous.›

lemma ccontinuous_all_x_imp_cont_global:
  assumes "∀x∈⋃τ⇩1. ∀U∈τ⇩2. f`x∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``V⊆U)" "f∈(⋃τ⇩1)→(⋃τ⇩2)"  and 
    "τ⇩1 {is a topology}"
  shows "IsContinuous(τ⇩1,τ⇩2,f)"
proof-
  {
    fix U
    assume "U∈τ⇩2"
    {
      fix x
      assume AS: "x∈f-``U"
      note ‹U∈τ⇩2›
      moreover
      from assms(2) have "f -`` U ⊆ ⋃τ⇩1" using func1_1_L6A by auto
      with AS have "x∈⋃τ⇩1" by auto
      with assms(1) have "∀U∈τ⇩2. f`x∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``V⊆U)" by auto
      moreover
      from AS assms(2) have "f`x∈U" using func1_1_L15 by auto
      ultimately have "∃V∈τ⇩1. x∈V ∧ f``V⊆U" by auto
      then obtain V where I: "V∈τ⇩1" "x∈V" "f``(V)⊆U" by auto
      moreover
      from I have "V⊆⋃τ⇩1" by auto
      moreover
      from assms(2) ‹V⊆⋃τ⇩1› have "V⊆f-``(f``V)" using func1_1_L9 by auto
      ultimately have "V ⊆ f-``(U)" by blast
      with ‹V∈τ⇩1› ‹x∈V› have "∃V∈τ⇩1. x∈V ∧ V ⊆ f-``(U)" by auto
    } hence "∀x∈f-``(U). ∃V∈τ⇩1. x∈V ∧ V⊆f-``(U)" by auto
    with assms(3) have "f-``(U) ∈ τ⇩1" using topology0.open_neigh_open topology0_def 
      by auto
  }
  hence "∀U∈τ⇩2. f-``U∈τ⇩1" by auto
  then show ?thesis using IsContinuous_def by auto
qed

subsection‹Continuous functions and filters›

text‹In this section we consider the relations between filters and continuity.› 

text‹If the function is continuous then 
  if the filter converges to a point the image filter converges to the image point.›

lemma (in two_top_spaces0) cont_imp_filter_conver_preserved:
  assumes "𝔉 {is a filter on} X⇩1" "f {is continuous}" "𝔉 →⇩F x {in} τ⇩1"
  shows "(f[𝔉]..X⇩2) →⇩F (f`(x)) {in} τ⇩2"
proof -
  from assms(1) assms(3) have "x∈X⇩1" 
    using topology0.FilterConverges_def topol_cntxs_valid(1) X1_def by auto
  have "topology0(τ⇩2)" using topol_cntxs_valid(2) by simp 
  moreover from assms(1) have "(f[𝔉]..X⇩2) {is a filter on} (⋃τ⇩2)" and "{f``B .B∈𝔉} {is a base filter} (f[𝔉]..X⇩2)" 
    using base_image_filter fmapAssum X1_def X2_def by auto
  moreover have "∀U∈Pow(⋃τ⇩2). (f`x)∈Interior(U,τ⇩2) ⟶ (∃D∈{f``B .B∈𝔉}. D⊆U)"
  proof - 
    { fix U
    assume "U∈Pow(X⇩2)" "(f`x)∈Interior(U,τ⇩2)"
    with ‹x∈X⇩1› have xim: "x∈f-``(Interior(U,τ⇩2))" and sub: "f-``(Interior(U,τ⇩2))∈Pow(X⇩1)" 
      using func1_1_L6A fmapAssum func1_1_L15 fmapAssum by auto
    note sub 
    moreover
    have "Interior(U,τ⇩2)∈τ⇩2" using topology0.Top_2_L2 topol_cntxs_valid(2) by auto
    with assms(2) have "f-``(Interior(U,τ⇩2))∈τ⇩1" unfolding isContinuous_def IsContinuous_def
      by auto
    with xim have "x∈Interior(f-``(Interior(U,τ⇩2)),τ⇩1)" 
      using topology0.Top_2_L3 topol_cntxs_valid(1) by auto
    moreover from assms(1) assms(3) have "{U∈Pow(X⇩1). x∈Interior(U,τ⇩1)}⊆𝔉" 
        using topology0.FilterConverges_def topol_cntxs_valid(1) X1_def by auto
    ultimately have "f-``(Interior(U,τ⇩2))∈𝔉" by auto
    moreover have "f``(f-``(Interior(U,τ⇩2)))⊆Interior(U,τ⇩2)" 
      using function_image_vimage fun_is_fun fmapAssum by auto
    then have "f``(f-``(Interior(U,τ⇩2)))⊆U" 
      using topology0.Top_2_L1 topol_cntxs_valid(2) by auto
    ultimately have "∃D∈{f``(B) .B∈𝔉}. D⊆U" by auto
    } thus ?thesis by auto 
  qed
  moreover from fmapAssum ‹x∈X⇩1›  have "f`(x) ∈ X⇩2"
    by (rule apply_funtype) 
  hence "f`(x) ∈ ⋃τ⇩2" by simp 
  ultimately show ?thesis by (rule topology0.convergence_filter_base2) 
qed

text‹Continuity in filter at every point of the domain implies global continuity.›

lemma (in two_top_spaces0) filter_conver_preserved_imp_cont:
  assumes "∀x∈⋃τ⇩1. ∀𝔉. ((𝔉 {is a filter on} X⇩1) ∧ (𝔉 →⇩F x {in} τ⇩1)) ⟶ ((f[𝔉]..X⇩2) →⇩F (f`x) {in} τ⇩2)"
  shows "f{is continuous}"
proof-
  {
    fix x
    assume as2: "x∈⋃τ⇩1"
    with assms have reg: 
      "∀𝔉. ((𝔉 {is a filter on} X⇩1) ∧ (𝔉 →⇩F x {in} τ⇩1)) ⟶ ((f[𝔉]..X⇩2) →⇩F (f`x) {in} τ⇩2)" 
      by auto
    let ?Neig = "{U ∈ Pow(⋃τ⇩1) . x ∈ Interior(U, τ⇩1)}"
    from as2 have NFil: "?Neig{is a filter on}X⇩1" and NCon: "?Neig →⇩F x {in} τ⇩1"
      using topol_cntxs_valid(1) topology0.neigh_filter by auto
    {
      fix U
      assume "U∈τ⇩2" "f`x∈U"
      then have "U∈Pow(⋃τ⇩2)" "f`x∈Interior(U,τ⇩2)" using topol_cntxs_valid(2) topology0.Top_2_L3 by auto
      moreover
      from NCon NFil reg have "(f[?Neig]..X⇩2) →⇩F (f`x) {in} τ⇩2" by auto 
      moreover have "(f[?Neig]..X⇩2) {is a filter on} X⇩2" 
        using base_image_filter(2) NFil fmapAssum by auto
      ultimately have "U∈(f[?Neig]..X⇩2)" 
        using topology0.FilterConverges_def topol_cntxs_valid(2) unfolding X1_def X2_def 
        by auto
      moreover
      from fmapAssum NFil have "{f``B .B∈?Neig} {is a base filter} (f[?Neig]..X⇩2)" 
        using base_image_filter(1) X1_def X2_def by auto
      ultimately have "∃V∈{f``B .B∈?Neig}. V⊆U" using basic_element_filter by blast
      then obtain B where "B∈?Neig" "f``B⊆U" by auto
      moreover
      have "Interior(B,τ⇩1)⊆B" using topology0.Top_2_L1 topol_cntxs_valid(1) by auto
      hence "f``Interior(B,τ⇩1) ⊆ f``(B)" by auto
      moreover have "Interior(B,τ⇩1)∈τ⇩1" 
        using topology0.Top_2_L2 topol_cntxs_valid(1) by auto
      ultimately have "∃V∈τ⇩1. x∈V ∧ f``V⊆U" by force
    }
    hence "∀U∈τ⇩2. f`x∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``V⊆U)" by auto
  }
  hence "∀x∈⋃τ⇩1. ∀U∈τ⇩2. f`x∈U ⟶ (∃V∈τ⇩1. x∈V ∧ f``V⊆U)" by auto
  then show ?thesis 
    using ccontinuous_all_x_imp_cont_global fmapAssum X1_def X2_def isContinuous_def tau1_is_top 
    by auto
qed

end