Theory UniformSpace_ZF_1

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

    Copyright (C) 2020 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 ‹ More on uniform spaces ›

theory UniformSpace_ZF_1 imports func_ZF_1 UniformSpace_ZF Topology_ZF_2
begin

text‹ This theory defines the maps to study in uniform spaces and proves their basic properties. ›

subsection‹ Uniformly continuous functions ›

text‹ Just as the the most general setting for continuity of functions is that of topological spaces, uniform spaces 
  are the most general setting for the study of uniform continuity. ›

text‹ A map between 2 uniformities is uniformly continuous if it preserves
the entourages: ›

definition
  IsUniformlyCont ("_ {is uniformly continuous between} _ {and} _" 90) where
  "f:X→Y ⟹ Φ {is a uniformity on} X  ⟹ Γ {is a uniformity on} Y ⟹ 
  f {is uniformly continuous between} Φ {and} Γ ≡ ∀V∈Γ. (ProdFunction(f,f)-``V) ∈ Φ"

text‹ Any uniformly continuous function is continuous when considering the topologies on the uniformities. ›

lemma uniformly_cont_is_cont:
  assumes "f:X→Y" "Φ {is a uniformity on} X " "Γ {is a uniformity on} Y" 
    "f {is uniformly continuous between} Φ {and} Γ"
  shows "IsContinuous(UniformTopology(Φ,X),UniformTopology(Γ,Y),f)"
proof -
  {  fix U assume op: "U ∈ UniformTopology(Γ,Y)"
    have "f-``(U) ∈ UniformTopology(Φ,X)"
    proof -
      from assms(1) have "f-``(U) ⊆ X" using func1_1_L3 by simp
      moreover 
      { fix x xa assume as:"⟨x,xa⟩ ∈ f" "xa ∈ U"
        with assms(1) have x:"x∈X" unfolding Pi_def by auto
        from as(2) op have U:"U ∈ {⟨t,{V``{t}.V∈Γ}⟩.t∈Y}`(xa)" using uniftop_def_alt by auto
        from as(1) assms(1) have xa:"xa ∈ Y" unfolding Pi_def by auto
        have "{⟨t,{V``{t}.V∈Γ}⟩.t∈Y} ∈ Pi(Y,%t. {{V``{t}.V∈Γ}})" unfolding Pi_def function_def 
          by auto
        with U xa have "U ∈{V``{xa}.V∈Γ}" using apply_equality by auto
        then obtain V where V:"U = V``{xa}" "V∈Γ" by auto
        with assms have ent:"(ProdFunction(f,f)-``(V))∈Φ" using IsUniformlyCont_def by simp
        have "∀t. t ∈ (ProdFunction(f,f)-``V)``{x} <-> ⟨x,t⟩ ∈ ProdFunction(f,f)-``(V)" 
          using image_def by auto
        with assms(1) x have "∀t. t: (ProdFunction(f,f)-``V)``{x} ⟷ (t∈X ∧ ⟨f`x,f`t⟩ ∈ V)" 
          using prodFunVimage by auto
        with assms(1) as(1) have "∀t. t ∈ (ProdFunction(f,f)-``V)``{x} ⟷ (t∈X ∧ ⟨xa,f`t⟩: V)" 
          using apply_equality by auto
        with V(1) have "∀t. t ∈ (ProdFunction(f,f)-``V)``{x} ⟷ (t∈X ∧ f`(t) ∈ U)" by auto
        with assms(1) U have "∀t. t ∈ (ProdFunction(f,f)-``V)``{x} ⟷ t ∈ f-``U"
          using func1_1_L15 by simp
        hence "f-``U = (ProdFunction(f,f)-``V)``{x}" by blast
        with ent have "f-``(U) ∈ {V``{x} . V ∈ Φ}" by auto 
        moreover
        have "{⟨t,{V``{t}.V∈Φ}⟩.t∈X} ∈ Pi(X,%t. {{V``{t}.V∈Φ}})" unfolding Pi_def function_def 
          by auto
        ultimately have "f-``(U) ∈ {⟨t, {V `` {t} . V ∈ Φ}⟩ . t ∈ X}`(x)" using x apply_equality 
          by auto
      } 
      ultimately show "f-``(U) ∈ UniformTopology(Φ,X)" using uniftop_def_alt by auto
    qed
  } then show ?thesis unfolding IsContinuous_def by simp
qed

end