theory MetricUniform_ZF_1 imports MetricUniform_ZF Real_ZF_2
begin
This theory continues MetricUniform_ZF specializing to the real valued pseudometrics. The ultimate goal is to show that every uniformity is the supremum of a collection of uniformities generated by a pseudometric. In this theory we show the AC-free fragments of the proof of this fact.
Metrization lemma
The metrization theorem states that a uniform space is pseudometrizable if and only if its uniformity has an countable base. In this sectiopn we show the key lemma that leads to the metrization theorem.
In the literature the metrization lemma (proven below) is usually stated as asserting existence of a pseudometric satisfying certain conditions. We prefer here a more explicit approach where we specify the construction of that pseudometric as a series of definitions, then show that the resulting function indeed satisfies the required conditions. The drawback of this approach is that we have to come up with names for the intermediate objects representing stages of that construction. Naming is hard, so as usual if the reader has an idea for better names please let me know.
We define the \( \text{DistWeight}(\mathcal{U} ,p) \) expression as equal to (real) \(0\) if \(p\in\bigcap_{n\in\mathbb{N}} \mathcal{U}_n\) or otherwise equal to \((\frac{1}{2})^n\), where \(n\) is the only natural number such that \(p\in\mathcal{U}_n\setminus\mathcal{U}_{n+1}\). To understand the context in which this definition is intended to be used suppose \(\mathcal{U}:\mathbb{N}\rightarrow \
(X\times X)\) is a sequence of subsets of \(X\times X\) such that \(\mathcal{U}_{n+1}\subseteq \mathcal{U}_n\) for \(n\in\mathbb{N}\). Then we have the identity \(\bigcup_{n\in mathbb{N}} (\mathcal{U}_n\setminus\mathcal{U}_{n+1})=\mathcal{U}_0\setminus \bigcap_{n\in mathbb{N}} \mathcal{U}_n\) and for any \(p\in\bigcup_{n\in mathbb{N}} (\mathcal{U}_n\setminus \mathcal{U}_{n+1})\) there is exactly one \(n\in mathbb{N}\) such that \(p\in \mathcal{U}_n\setminus \mathcal{U}_{n+1}\) This means that the set \(\{n\in n\in mathbb{N}: p\in \mathcal{U}_n\setminus \mathcal{U}_{n+1}\}\) is a singleton and we can use the \(\bigcup \{ x\} = x\) identity to extract its only element.
definition (in reals)
\( \text{DistWeight}(\mathcal{U} ,p) \equiv \text{if }p \in (\bigcap n\in nat.\ \mathcal{U} (n))\text{ then } 0 \text{ else }(\ \lt onehalf>)^{\bigcup \{n\in nat.\ p\in (\mathcal{U} (n)\setminus \mathcal{U} (n + 1))\}} \)
Suppose \(\mathcal{U}:\mathbb{N}\rightarrow \
(X\times X)\) is a sequence of subsets of \(X\times X\) such that \(\mathcal{U}_{n+1}\subseteq \mathcal{U}_n\) for all \(n\in\mathbb{N}\). Assume further that \(p\in\mathcal{U}_n\setminus \mathcal{U}_{n+1}\) for some \(n\in\mathbb{N}\). Then \( \text{DistWeight}(\mathcal{U} ,p) \) is equal to \(\left(frac{1}{2}\right)^n\).
lemma (in reals) dist_weight_val:
assumes \( \mathcal{U} :nat\rightarrow Pow(X\times X) \), \( \forall i\in nat.\ \mathcal{U} (i + 1) \subseteq \mathcal{U} (i) \) and \( n\in nat \), \( p \in (\mathcal{U} (n)\setminus \mathcal{U} (n + 1)) \)
shows \( \text{DistWeight}(\mathcal{U} ,p) = (\ \lt onehalf>)^{n} \)proof let \( \mathcal{V} = \{\langle i,\mathcal{U} (i)\setminus \mathcal{U} (i + 1)\rangle .\ i\in nat\} \)
have I: \( \forall i\in nat.\ \mathcal{V} (i) = \mathcal{U} (i)\setminus \mathcal{U} (i + 1) \) using ZF_fun_from_tot_val2
from assms(1,2) have \( \mathcal{V} :nat\rightarrow Pow(X\times X) \), \( \mathcal{V} \text{ is pairwise disjoint } \) and II: \( (\bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1)) = \mathcal{U} (0)\setminus (\bigcap n\in nat.\ \mathcal{U} (n)) \) using decr_pair_disj1(1,3,4)
from assms(3,4), I have \( p\in \mathcal{V} (n) \)
with assms(3), \( \mathcal{V} :nat\rightarrow Pow(X\times X) \), \( \mathcal{V} \text{ is pairwise disjoint } \) have \( n = \bigcup \{i\in nat.\ p\in \mathcal{V} (i)\} \) using get_the_one
with assms(3,4), I have \( n = \bigcup \{i\in nat.\ p\in \mathcal{U} (i)\setminus \mathcal{U} (i + 1)\} \) and \( p \in (\bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1)) \)
with II show \( thesis \) unfolding DistWeight_def
qed
end
lemma ZF_fun_from_tot_val2: shows \( \forall x\in X.\ \{\langle x,b(x)\rangle .\ x\in X\}(x) = b(x) \)
lemma decr_pair_disj1:
assumes \( \mathcal{U} :nat\rightarrow Pow(X) \), \( \forall n\in nat.\ \mathcal{U} (n + 1)\subseteq \mathcal{U} (n) \)
defines \( \mathcal{V} \equiv \{\langle i,\mathcal{U} (i)\setminus \mathcal{U} (i + 1)\rangle .\ i\in nat\} \)
shows \( \mathcal{V} :nat\rightarrow Pow(X) \), \( \text{IsDecreasingSeq}(Pow(X), \text{InclusionOn}(Pow(X)),\mathcal{U} ) \), \( \mathcal{V} \text{ is pairwise disjoint } \), \( (\bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1)) = \mathcal{U} (0)\setminus (\bigcap n\in nat.\ \mathcal{U} (n)) \) lemma get_the_one:
assumes \( X:I\rightarrow Y \), \( X \text{ is pairwise disjoint } \), \( i\in I \), \( x\in X(i) \)
shows \( i = \bigcup \{j\in I.\ x\in X(j)\} \)Definition of DistWeight:
\( \text{DistWeight}(\mathcal{U} ,p) \equiv \text{if }p \in (\bigcap n\in nat.\ \mathcal{U} (n))\text{ then } 0 \text{ else }(\ \lt onehalf>)^{\bigcup \{n\in nat.\ p\in (\mathcal{U} (n)\setminus \mathcal{U} (n + 1))\}} \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
