IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory UniformSpace_ZF_1 imports func_ZF_1 UniformSpace_ZF Topology_ZF_2

begin

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

Uniformly continuous functions

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.

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

definition

\( f:X\rightarrow Y \Longrightarrow \Phi \text{ is a uniformity on } X \Longrightarrow \Gamma \text{ is a uniformity on } Y \Longrightarrow \) \( f \text{ is uniformly continuous between } \Phi \text{ and } \Gamma \equiv \forall V\in \Gamma .\ ( \text{ProdFunction}(f,f)^{-1}V) \in \Phi \)

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

lemma uniformly_cont_is_cont:

assumes \( f:X\rightarrow Y \), \( \Phi \text{ is a uniformity on } X \), \( \Gamma \text{ is a uniformity on } Y \), \( f \text{ is uniformly continuous between } \Phi \text{ and } \Gamma \)

shows \( \text{IsContinuous}( \text{UniformTopology}(\Phi ,X), \text{UniformTopology}(\Gamma ,Y),f) \)proof

{

fix \( U \)

assume op: \( U \in \text{UniformTopology}(\Gamma ,Y) \)

have \( f^{-1}(U) \in \text{UniformTopology}(\Phi ,X) \)proof

from assms(1) have \( f^{-1}(U) \subseteq X \) using func1_1_L3

moreover {

fix \( x \) \( xa \)

assume as: \( \langle x,xa\rangle \in f \), \( xa \in U \)

with assms(1) have x: \( x\in X \) unfolding Pi_def

from as(2), op have U: \( U \in \{\langle t,\{V\{t\}.\ V\in \Gamma \}\rangle .\ t\in Y\}(xa) \) using uniftop_def_alt

from as(1), assms(1) have xa: \( xa \in Y \) unfolding Pi_def

have \( \{\langle t,\{V\{t\}.\ V\in \Gamma \}\rangle .\ t\in Y\} \in \text{Pi}(Y,\%t.\ \{\{V\{t\}.\ V\in \Gamma \}\}) \) unfolding Pi_def, function_def

with U, xa have \( U \in \{V\{xa\}.\ V\in \Gamma \} \) using apply_equality

then obtain \( V \) where V: \( U = V\{xa\} \), \( V\in \Gamma \)

with assms have ent: \( ( \text{ProdFunction}(f,f)^{-1}(V))\in \Phi \) using IsUniformlyCont_def

have \( \forall t.\ t \in ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \lt -> \langle x,t\rangle \in \text{ProdFunction}(f,f)^{-1}(V) \) using image_def

with assms(1), x have \( \forall t.\ t: ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \longleftrightarrow (t\in X \wedge \langle fx,ft\rangle \in V) \) using prodFunVimage

with assms(1), as(1) have \( \forall t.\ t \in ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \longleftrightarrow (t\in X \wedge \langle xa,ft\rangle : V) \) using apply_equality

with V(1) have \( \forall t.\ t \in ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \longleftrightarrow (t\in X \wedge f(t) \in U) \)

with assms(1), U have \( \forall t.\ t \in ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \longleftrightarrow t \in f^{-1}U \) using func1_1_L15

hence \( f^{-1}U = ( \text{ProdFunction}(f,f)^{-1}V)\{x\} \)

with ent have \( f^{-1}(U) \in \{V\{x\} .\ V \in \Phi \} \)

moreover

have \( \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\} \in \text{Pi}(X,\%t.\ \{\{V\{t\}.\ V\in \Phi \}\}) \) unfolding Pi_def, function_def

ultimately have \( f^{-1}(U) \in \{\langle t, \{V \{t\} .\ V \in \Phi \}\rangle .\ t \in X\}(x) \) using x, apply_equality

} ultimately show \( f^{-1}(U) \in \text{UniformTopology}(\Phi ,X) \) using uniftop_def_alt

qed

}

then show \( thesis \) unfolding IsContinuous_def

qed

end

lemma func1_1_L3:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(D) \subseteq X \)

lemma uniftop_def_alt: shows \( \text{UniformTopology}(\Phi ,X) = \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\} \)

Definition of IsUniformlyCont: \( f:X\rightarrow Y \Longrightarrow \Phi \text{ is a uniformity on } X \Longrightarrow \Gamma \text{ is a uniformity on } Y \Longrightarrow \) \( f \text{ is uniformly continuous between } \Phi \text{ and } \Gamma \equiv \forall V\in \Gamma .\ ( \text{ProdFunction}(f,f)^{-1}V) \in \Phi \)

lemma prodFunVimage:

assumes \( x\in X \), \( f:X\rightarrow Y \)

shows \( \langle x,t\rangle \in \text{ProdFunction}(f,f)^{-1}(V) \longleftrightarrow t\in X \wedge \langle fx,ft\rangle \in V \)

lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)

Definition of IsContinuous: \( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)