theory UniformSpace_ZF imports Topology_ZF_4a
begin
This theory defines uniform spaces and proves their basic properties.
Definition and motivation
Just like a topological space constitutes the minimal setting in which one can speak of continuous functions, the notion of uniform spaces (commonly attributed to André Weil) captures the minimal setting in which one can speak of uniformly continuous functions. In some sense this is a generalization of the notion of metric (or metrizable) spaces and topological groups.
There are several definitions of uniform spaces. The fact that these definitions are equivalent is far from obvious (some people call such phenomenon cryptomorphism). We will use the definition of the uniform structure (or ''uniformity'') based on entourages. This was the original definition by Weil and it seems to be the most commonly used. A uniformity consists of entourages that are binary relations between points of space \(X\) that satisfy a certain collection of conditions, specified below.
Definition
\( \Phi \text{ is a uniformity on } X \equiv (\Phi \text{ is a filter on } (X\times X))\) \( \wedge (\forall U\in \Phi .\ id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi ) \)
A Member of a uniformity on \(X\) is a reflexive relation on \(X\).
lemma unif_props:
assumes \( \Phi \text{ is a uniformity on } X \), \( A\in \Phi \)
shows \( A \subseteq X\times X \) and \( id(X) \subseteq A \) using assms, IsUniformity_def, IsFilter_defThe definition of uniformity states (among other things) that for every member \(U\) of uniformity \(\Phi\) there is another one, say \(V\) such that \(V\circ V\subseteq U\). Sometimes such \(V\) is said to be half the size of \(U\). The next lemma states that \(V\) can be taken to be symmetric.
lemma half_size_symm:
assumes \( \Phi \text{ is a uniformity on } X \), \( U\in \Phi \)
shows \( \exists W\in \Phi .\ W\circ W \subseteq U \wedge W=converse(W) \)proof from assms obtain \( V \) where \( V\in \Phi \) and \( V\circ V \subseteq U \) unfolding IsUniformity_def
let \( W = V \cap converse(V) \)
from assms(1), \( V\in \Phi \) have \( W \in \Phi \) and \( W = converse(W) \) unfolding IsUniformity_def, IsFilter_def
moreover
qed
from \( V\circ V \subseteq U \) have \( W\circ W \subseteq U \)
ultimately show \( thesis \)
If \(\Phi\) is a uniformity on \(X\), then the every element \(V\) of \(\Phi\) is a certain relation on \(X\) (a subset of \(X\times X\)) and is called an ''entourage''. For an \(x\in X\) we call \(V\{ x\}\) a neighborhood of \(x\). The first useful fact we will show is that neighborhoods are non-empty.
lemma neigh_not_empty:
assumes \( \Phi \text{ is a uniformity on } X \), \( V\in \Phi \) and \( x\in X \)
shows \( V\{x\} \neq 0 \) and \( x \in V\{x\} \)proof from assms(1,2) have \( id(X) \subseteq V \) using IsUniformity_def, IsFilter_def
with \( x\in X \) show \( x\in V\{x\} \) and \( V\{x\} \neq 0 \)
qed
If \(\Phi\) is a uniformity on \(X\) then every element of \(\Phi\) is a subset of \(X\times X\) whose domain is \(x\).
lemma uni_domain:
assumes \( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)
shows \( W \subseteq X\times X \) and \( domain(W) = X \)proof from assms show \( W \subseteq X\times X \) unfolding IsUniformity_def, IsFilter_def
show \( domain(W) = X \)proof
qed
from assms show \( domain(W) \subseteq X \) unfolding IsUniformity_def, IsFilter_def
from assms show \( X \subseteq domain(W) \) unfolding IsUniformity_def
qed
Uniformity \( \Phi \) defines a natural topology on its space \(X\) via the neighborhood system that assigns the collection \(\{V(\{x\}):V\in \Phi\}\) to every point \(x\in X\). In the next lemma we show that if we define a function this way the values of that function are what they should be. This is only a technical fact which is useful to shorten the remaining proofs, usually treated as obvious in standard mathematics.
lemma neigh_filt_fun:
assumes \( \Phi \text{ is a uniformity on } X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \)proof from assms have \( \forall x\in X.\ \{V\{x\}.\ V\in \Phi \} \in Pow(Pow(X)) \) using IsUniformity_def, IsFilter_def, image_subset
with assms show \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) using ZF_fun_from_total
with assms show \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) using ZF_fun_from_tot_val
qed
In the next lemma we show that the collection defined in lemma neigh_filt_fun is a filter on \(X\). The proof is kind of long, but it just checks that all filter conditions hold.
lemma filter_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \) and \( x\in X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} (x) \text{ is a filter on } X \)proof from assms have PhiFilter: \( \Phi \text{ is a filter on } (X\times X) \) and \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) using IsUniformity_def, neigh_filt_fun
have \( 0 \notin \mathcal{M} (x) \)proof
from assms, \( x\in X \) have \( 0 \notin \{V\{x\}.\ V\in \Phi \} \) using neigh_not_empty
with \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) show \( 0 \notin \mathcal{M} (x) \)
qed
moreover
qed
have \( X \in \mathcal{M} (x) \)proof
moreover note \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \)
moreover
qed
from assms have \( X\times X \in \Phi \) unfolding IsUniformity_def, IsFilter_def
hence \( (X\times X)\{x\} \in \{V\{x\}.\ V\in \Phi \} \)
moreover from \( x\in X \) have \( (X\times X)\{x\} = X \)
ultimately show \( X \in \mathcal{M} (x) \)
from \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), \( x\in X \) have \( \mathcal{M} (x) \subseteq Pow(X) \) using apply_funtype
moreover have LargerIn: \( \forall B \in \mathcal{M} (x).\ \forall C \in Pow(X).\ B\subseteq C \longrightarrow C \in \mathcal{M} (x) \)proof
moreover {
}
fix \( B \)
assume \( B \in \mathcal{M} (x) \)
fix \( C \)
assume \( C \in Pow(X) \) and \( B\subseteq C \)
from \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \), \( B \in \mathcal{M} (x) \) obtain \( U \) where \( U\in \Phi \) and \( B = U\{x\} \)
let \( V = U \cup C\times C \)
from assms, \( U\in \Phi \), \( C \in Pow(X) \) have \( V \in Pow(X\times X) \) and \( U\subseteq V \) using IsUniformity_def, IsFilter_def
with \( U\in \Phi \), PhiFilter have \( V\in \Phi \) using IsFilter_def
moreover
from assms, \( U\in \Phi \), \( x\in X \), \( B = U\{x\} \), \( B\subseteq C \) have \( C = V\{x\} \) using neigh_not_empty, image_greater_rel
ultimately have \( C \in \{V\{x\}.\ V\in \Phi \} \)
with \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) have \( C \in \mathcal{M} (x) \)
thus \( thesis \)
qed
have \( \forall A \in \mathcal{M} (x).\ \forall B \in \mathcal{M} (x).\ A\cap B \in \mathcal{M} (x) \)proof
ultimately show \( thesis \) unfolding IsFilter_def
{
}
fix \( A \) \( B \)
assume \( A \in \mathcal{M} (x) \) and \( B \in \mathcal{M} (x) \)
with \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) obtain \( V_A \) \( V_B \) where \( A = V_A\{x\} \), \( B = V_B\{x\} \) and \( V_A \in \Phi \), \( V_B \in \Phi \)
let \( C = V_A\{x\} \cap V_B\{x\} \)
from assms, \( V_A \in \Phi \), \( V_B \in \Phi \) have \( V_A\cap V_B \in \Phi \) using IsUniformity_def, IsFilter_def
with \( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) have \( (V_A\cap V_B)\{x\} \in \mathcal{M} (x) \)
moreover
from PhiFilter, \( V_A \in \Phi \), \( V_B \in \Phi \) have \( C \in Pow(X) \) unfolding IsFilter_def
moreover have \( (V_A\cap V_B)\{x\} \subseteq C \) using image_Int_subset_left
moreover note LargerIn
ultimately have \( C \in \mathcal{M} (x) \)
with \( A = V_A\{x\} \), \( B = V_B\{x\} \) have \( A\cap B \in \mathcal{M} (x) \)
thus \( thesis \)
qed
The function defined in the premises of lemma neigh_filt_fun (or filter_from_uniformity) is a neighborhood system. The proof uses the existence of the "half-the-size" neighborhood condition (\( \exists V\in \Phi .\ V\circ V \subseteq U \)) of the uniformity definition, but not the \( converse(U) \in \Phi \) part.
theorem neigh_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X \)proof let \( \mathcal{M} = \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
from assms have \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and Mval: \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) using IsUniformity_def, neigh_filt_fun
moreover
}
ultimately show \( thesis \) unfolding IsNeighSystem_def
qed
from assms have \( \forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \) using filter_from_uniformity
moreover {
fix \( x \)
assume \( x\in X \)
have \( \forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y))) \)proof
{
}
fix \( N \)
assume \( N\in \mathcal{M} (x) \)
have \( x\in N \) and \( \exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N \in \mathcal{M} (y)) \)proof
from \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), Mval, \( x\in X \), \( N\in \mathcal{M} (x) \) obtain \( U \) where \( U\in \Phi \) and \( N = U\{x\} \)
with assms, \( x\in X \) show \( x\in N \) using neigh_not_empty
from assms, \( U\in \Phi \) obtain \( V \) where \( V\in \Phi \) and \( V\circ V \subseteq U \) unfolding IsUniformity_def
let \( W = V\{x\} \)
from \( V\in \Phi \), Mval, \( x\in X \) have \( W \in \mathcal{M} (x) \)
moreover
qed
have \( \forall y\in W.\ N \in \mathcal{M} (y) \)proof
ultimately show \( \exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N \in \mathcal{M} (y)) \)
{
}
fix \( y \)
assume \( y\in W \)
with \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), \( x\in X \), \( W \in \mathcal{M} (x) \) have \( y\in X \) using apply_funtype
with assms have \( \mathcal{M} (y) \text{ is a filter on } X \) using filter_from_uniformity
moreover
from assms, \( y\in X \), \( V\in \Phi \) have \( V\{y\} \in \mathcal{M} (y) \) using neigh_filt_fun
moreover from \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), \( x\in X \), \( N \in \mathcal{M} (x) \) have \( N \in Pow(X) \) using apply_funtype
moreover from \( V\circ V \subseteq U \), \( y\in W \) have \( V\{y\} \subseteq (V\circ V)\{x\} \) and \( (V\circ V)\{x\} \subseteq U\{x\} \)
with \( N = U\{x\} \) have \( V\{y\} \subseteq N \)
ultimately have \( N \in \mathcal{M} (y) \) unfolding IsFilter_def
thus \( thesis \)
qed
thus \( thesis \)
qed
When we have a uniformity \(\Phi\) on \(X\) we can define a topology on \(X\) in a (relatively) natural way. We will call that topology the \( \text{UniformTopology}(\Phi ) \). The definition may be a bit cryptic but it just combines the construction of a neighborhood system from uniformity as in the assumptions of lemma filter_from_uniformity and the construction of topology from a neighborhood system from theorem topology_from_neighs. We could probably reformulate the definition to skip the \(X\) parameter because if \(\Phi\) is a uniformity on \(X\) then \(X\) can be recovered from (is determined by) \(\Phi\).
Definition
\( \text{UniformTopology}(\Phi ,X) \equiv \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\} \)
The collection of sets constructed in the UniformTopology definition is indeed a topology on \(X\).
theorem uniform_top_is_top:
assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \text{UniformTopology}(\Phi ,X) \text{ is a topology } \) and \( \bigcup \text{UniformTopology}(\Phi ,X) = X \) using assms, neigh_from_uniformity, UniformTopology_def, topology_from_neighs end
Definition of IsUniformity:
\( \Phi \text{ is a uniformity on } X \equiv (\Phi \text{ is a filter on } (X\times X))\)
\( \wedge (\forall U\in \Phi .\ id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi ) \)
Definition of IsFilter:
\( \mathfrak{F} \text{ is a filter on } X \equiv (0\notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge (\mathfrak{F} \subseteq Pow(X)) \wedge \)
\( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)
lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma ZF_fun_from_tot_val:
assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) lemma neigh_filt_fun:
assumes \( \Phi \text{ is a uniformity on } X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) lemma neigh_not_empty:
assumes \( \Phi \text{ is a uniformity on } X \), \( V\in \Phi \) and \( x\in X \)
shows \( V\{x\} \neq 0 \) and \( x \in V\{x\} \) lemma image_greater_rel:
assumes \( x \in U\{x\} \) and \( U\{x\} \subseteq C \)
shows \( (U \cup C\times C)\{x\} = C \) lemma filter_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \) and \( x\in X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} (x) \text{ is a filter on } X \)Definition of IsNeighSystem:
\( \mathcal{M} \text{ is a neighborhood system on } X \equiv (\mathcal{M} : X\rightarrow Pow(Pow(X))) \wedge \)
\( (\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \wedge (\forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) ) )) \)
theorem neigh_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X \)Definition of UniformTopology:
\( \text{UniformTopology}(\Phi ,X) \equiv \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\} \)
theorem topology_from_neighs:
assumes \( \mathcal{M} \text{ is a neighborhood system on } X \)
defines \( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)
shows \( T \text{ is a topology } \) and \( \bigcup T = X \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8