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) \)