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.
Defining pseudometrics with weighted chains
This section describes a method of defining real valued pseudometrics through infimum of the set of weights of all chains connecting two points. The notions of chains and links are defined in the FiniteSeq_ZF theory, with some properties proven in the Monoid_ZF_1 theory.
Since we will be using the set of non-zero natural numbers quite a lot, let's denote it \(\mathbb{N}_1\)
abbreviation
\( \mathbb{N} _1 \equiv nat\setminus \{0\} \)
In the monoid1 context we have defined a notion of ChainWeight. The next definition brings that notion into the reals context
definition (in reals)
\( \text{RChainWeight}(w,c) \equiv monoid1.\ \text{ChainWeight}(\mathbb{R} ,Add,w,c) \)
Given a chain of elements of \(X\) and a weight function \(w:X\times X\rightarrow \mathbb{R}\) the weight of a chain is a real number.
lemma (in reals) chain_weight_real:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow \mathbb{R} \)
shows \( \text{RChainWeight}(w,c) \in \mathbb{R} \) using assms, chain_weight_type unfolding RChainWeight_defGiven a weight function \(w:X\rightarrow \mathbb{R}^+\) we define the chain distance between two points \(x,y\in X\) as the infimum of set of weights of all chains of nonzero length connecting \(x\) and \(y\).
definition (in reals)
\( \text{ChainDist}(X,w,x,y) \equiv inf(\{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y))\}) \)
If the weight function is valued in nonnegative real numbers then the weight of every chain in nonnegative.
lemma (in reals) chain_weight_nonneg:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \text{RChainWeight}(w,c) \in \mathbb{R} ^+ \)proof from assms have \( w\circ \text{ChainLinks}(c) : n\rightarrow \mathbb{R} ^+ \) using chain_links_fun(2), comp_fun
with assms(1) have \( (\sum (w\circ \text{ChainLinks}(c))) \in \mathbb{R} ^+ \) using loop1_valid_in_group3, sum_nonneg_nonneg
then show \( \text{RChainWeight}(w,c) \in \mathbb{R} ^+ \) using monoid1_valid_in_group, ChainWeight_def unfolding RChainWeight_def
qed
If the weight function is nonnegative then the set of weights of all nontrivial chains in \(X\) connecting \(x\) and \(y\) is contained in nonnegative reals.
corollary (in reals) chain_weights_nonneg:
assumes \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y))\} \subseteq \mathbb{R} ^+ \) using assms, chain_weight_nonnegThe chain_concat_weight1 lemma from the monoid1 context rewritten using notation used in the reals context:
lemma (in reals) rchain_concat_weight:
assumes \( w:X\times X\rightarrow \mathbb{R} \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \), \( c_1\in \text{Chains}(X,n_1,x,y) \), \( c_2\in \text{Chains}(X,n_2,y,z) \) and \( n_1\in nat \), \( n_2\in nat \)
shows \( \text{RChainWeight}(w, \text{Concat}(c_1,c_2)) = \text{RChainWeight}(w,c_1) + \text{RChainWeight}(w,c_2) \) using assms, monoid1_valid_in_group, chain_concat_weight1 unfolding RChainWeight_defIf the weight function is nonnegative then the chain distance is also nonnegative.
lemma (in reals) chain_dist_nneg:
assumes \( x\in X \), \( y\in X \) and \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \text{ChainDist}(X,w,x,y) \in \mathbb{R} ^+ \) using assms, chains_nempty(4), chain_weights_nonneg, nneg_has_nneg_inf unfolding ChainDist_defIf the weight function is nonnegative and zero on the diagonal then the chain distance obeys the triangle inequality.
lemma (in reals) chain_dist_tr_ineq:
assumes \( x\in X \), \( y\in X \), \( z\in X \) and \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \)
shows \( \text{ChainDist}(X,w,x,z) \leq \text{ChainDist}(X,w,x,y) + \text{ChainDist}(X,w,y,z) \)proof let \( W_1 = \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y))\} \)
let \( W_2 = \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,y,z))\} \)
let \( W_3 = \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,z))\} \)
let \( W_4 = \{w_1 + w_2.\ \langle w_1,w_2\rangle \in W_1\times W_2\} \)
from R_are_reals, assms(1,2,3,4) have \( W_1\neq \emptyset \), \( W_2\neq \emptyset \), \( W_3\neq \emptyset \), \( W_4\neq \emptyset \), \( \text{antisym}(ROrd) \), \( w:X\times X\rightarrow \mathbb{R} \) using chains_nempty(4), cart_prod_nempty, OrderedGroup_ZF_1_L4E, func1_1_L1B unfolding IsAmodelOfReals_def, IsAnOrdField_def, IsAnOrdRing_def, IsLinOrder_def
have \( W_4 \subseteq W_3 \)proof
fix \( v \)
assume \( v \in \{w_1 + w_2.\ \langle w_1,w_2\rangle \in W_1\times W_2\} \)
then obtain \( w_1 \) \( w_2 \) where \( w_1\in W_1 \), \( w_2\in W_2 \) and \( v = w_1 + w_2 \)
from \( w_1\in W_1 \), \( w_2\in W_2 \) obtain \( c_1 \) \( c_2 \) where I: \( w_1 = \text{RChainWeight}(w,c_1) \), \( w_2 = \text{RChainWeight}(w,c_2) \) and II: \( c_1\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y)) \), \( c_2\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,y,z)) \)
let \( c_3 = \text{Concat}(c_1,c_2) \)
have \( c_3 \in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,z)) \) and \( \text{RChainWeight}(w,c_3) = v \)proof
from II obtain \( n_1 \) \( n_2 \) where \( n_1\in \mathbb{N} _1 \), \( n_2\in \mathbb{N} _1 \) and III: \( c_1 \in \text{Chains}(X,n_1,x,y) \), \( c_2 \in \text{Chains}(X,n_2,y,z) \)
from assms(5), \( n_1\in \mathbb{N} _1 \), \( n_2\in \mathbb{N} _1 \), \( w:X\times X\rightarrow \mathbb{R} \), III have \( n_1\in nat \), \( n_2\in nat \), \( n_1 + n_2 + 1 \in \mathbb{N} _1 \) and \( \text{RChainWeight}(w,c_3) = \text{RChainWeight}(w,c_1) + \text{RChainWeight}(w,c_2) \) using rchain_concat_weight
with \( v = w_1 + w_2 \), I show \( \text{RChainWeight}(w,c_3) = v \)
from \( n_1\in nat \), \( n_2\in nat \), III, \( n_1 + n_2 + 1 \in \mathbb{N} _1 \) show \( c_3 \in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,z)) \) using concat_chains(1)
qed
thus \( v\in W_3 \)
qed
from assms(4), \( W_4 \subseteq W_3 \) have \( W_1\subseteq \mathbb{R} ^+ \), \( W_2\subseteq \mathbb{R} ^+ \), \( W_3\subseteq \mathbb{R} ^+ \) using chain_weight_nonneg
from \( W_4\subseteq W_3 \), \( W_3\subseteq \mathbb{R} ^+ \) have \( W_4\subseteq \mathbb{R} ^+ \)
from \( W_3\neq \emptyset \), \( W_3\subseteq \mathbb{R} ^+ \), \( W_4\neq \emptyset \), \( W_4\subseteq \mathbb{R} ^+ \), \( \text{antisym}(ROrd) \), \( W_4 \subseteq W_3 \) have \( inf(W_3)\leq inf(W_4) \) using nneg_has_nneg_inf(1), inf_incl_mono
with \( W_1\neq \emptyset \), \( W_1\subseteq \mathbb{R} ^+ \), \( W_2\neq \emptyset \), \( W_2\subseteq \mathbb{R} ^+ \) show \( thesis \) using nonneg_inf_sum_inf(2) unfolding ChainDist_def
qed
If the weight function vanishes on the diagonal then the chain distance from \(x\in X\) to \(x\) is zero.
lemma (in reals) chain_dist_self_zero:
assumes \( x\in X \), \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( w\langle x,x\rangle = 0 \)
shows \( \text{ChainDist}(X,w,x,x) = 0 \)proof let \( c = \{\langle 0,x\rangle ,\langle 1,x\rangle \} \)
from assms(1) have I: \( c \in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,x)) \) using chains_nempty(1)
from assms have \( \text{RChainWeight}(w,c) = 0 \) using OrderedGroup_ZF_1_L4E, func1_1_L1B, monoid1_valid_in_group, weight_one_link unfolding RChainWeight_def
with I have \( 0 \in \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,x))\} \)
with assms(2) show \( \text{ChainDist}(X,w,x,x) = 0 \) using chain_weights_nonneg, loop1_valid_in_group3, zero_subset_nneg(4) unfolding ChainDist_def
qed
If the weight function is symmetric then the chain distance from \(x\) to \(y\) is the same as from \(y\) to \(x\).
lemma (in reals) chain_dist_symm:
assumes \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( \forall x\in X.\ \forall y\in X.\ w\langle x,y\rangle = w\langle y,x\rangle \)
shows \( \text{ChainDist}(X,w,x,y) = \text{ChainDist}(X,w,y,x) \) using assms, basic_props(2), OrderedGroup_ZF_1_L4E, func1_1_L1B, monoid1_valid_in_group, weight_set_rev_eq unfolding RChainWeight_def, ChainDist_defGiven a weight function \(w\rightarrow X\times X\) we define the chain weight pseudometric as a function on \(X\times X\) that assigns the chain distance to any pair \(\langle x,y\rangle \in X\times X\).
definition (in reals)
\( \text{ChainWeightPMetric}(X,w) \equiv \{\langle p, \text{ChainDist}(X,w,\text{fst}(p),\text{snd}(p))\rangle .\ p \in X\times X\} \)
If \(w:X\times X\rightarrow\mathbb{R}^+\) is symmetric and vanishes on the diagonal of \(X\times X\) then the chain weight pseudometric derived from \(w\) is indeed a real-valued pseudometric.
theorem (in reals) chain_weight_pmetric:
assumes \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \), \( \forall x\in X.\ \forall y\in X.\ w\langle x,y\rangle = w\langle y,x\rangle \)
shows \( \text{IsApseudoMetric}( \text{ChainWeightPMetric}(X,w),X,\mathbb{R} ,Add,ROrd) \) using assms, ZF_fun_from_total, chain_dist_nneg, ZF_fun_from_tot_val1, chain_dist_self_zero, chain_dist_symm, chain_dist_tr_ineq unfolding ChainWeightPMetric_def, IsApseudoMetric_defMetrization 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\mathcal{P}(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 }( \frac{1}{2} )^{\bigcup \{n\in nat.\ p\in (\mathcal{U} (n)\setminus \mathcal{U} (n + 1))\}} \)
Suppose \(\mathcal{U}:\mathbb{N}\rightarrow \mathcal{P}(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) = ( \frac{1}{2} )^{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 (in monoid1) chain_weight_type:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w,c) \in G \)Definition of RChainWeight:
\( \text{RChainWeight}(w,c) \equiv monoid1.\ \text{ChainWeight}(\mathbb{R} ,Add,w,c) \)
lemma chain_links_fun:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( domain(c) - 1 = n \) and \( \text{ChainLinks}(c):n\rightarrow X\times X \) lemma (in group3) loop1_valid_in_group3: shows \( loop1(G,P,r) \)
lemma (in loop1) sum_nonneg_nonneg:
assumes \( n\in nat \), \( s:n\rightarrow L^+ \)
shows \( (\sum s) \in L^+ \) lemma (in group0) monoid1_valid_in_group: shows \( monoid1(G,P) \)
Definition of ChainWeight:
\( \text{ChainWeight}(w,c) \equiv \sum (w\circ \text{ChainLinks}(c)) \)
lemma (in reals) chain_weight_nonneg:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \text{RChainWeight}(w,c) \in \mathbb{R} ^+ \) lemma (in monoid1) chain_concat_weight1:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x,y) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,y,z) \) and \( w:X\times X\rightarrow G \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \)
shows \( \text{ChainWeight}(w, \text{Concat}(c_1,c_2)) = \text{ChainWeight}(w,c_1)\oplus \text{ChainWeight}(w,c_2) \) lemma chains_nempty:
assumes \( x\in X \) and \( y\in X \)
shows \( \{\langle 0,x\rangle ,\langle 1,y\rangle \} \in \text{Chains}(X,1,x,y) \), \( \{\langle 0,x\rangle ,\langle 1,y\rangle \}(0) = x \), \( \{\langle 0,x\rangle ,\langle 1,y\rangle \}(1) = y \), \( (\bigcup n\in nat\setminus \{0\}.\ \text{Chains}(X,n,x,y)) \neq \emptyset \) corollary (in reals) chain_weights_nonneg:
assumes \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y))\} \subseteq \mathbb{R} ^+ \) lemma (in reals) nneg_has_nneg_inf:
assumes \( A\neq \emptyset \), \( A\subseteq \mathbb{R} ^+ \)
shows \( A \text{ has an infimum } \) and \( inf(A) \in \mathbb{R} ^+ \)Definition of ChainDist:
\( \text{ChainDist}(X,w,x,y) \equiv inf(\{ \text{RChainWeight}(w,c).\ c\in (\bigcup n\in \mathbb{N} _1.\ \text{Chains}(X,n,x,y))\}) \)
lemma cart_prod_nempty:
assumes \( A\neq \emptyset \), \( B\neq \emptyset \)
shows \( \{b(x,y).\ \langle x,y\rangle \in A\times B\} \neq \emptyset \) lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
lemma func1_1_L1B:
assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)
shows \( f:X\rightarrow Z \)Definition of IsAmodelOfReals:
\( \text{IsAmodelOfReals}(K,A,M,r) \equiv \text{IsAnOrdField}(K,A,M,r) \wedge (r \text{ is complete }) \)
Definition of IsAnOrdField:
\( \text{IsAnOrdField}(K,A,M,r) \equiv ( \text{IsAnOrdRing}(K,A,M,r) \wedge \)
\( (M \text{ is commutative on } K) \wedge \)
\( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \)
\( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \)
\( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
Definition of IsAnOrdRing:
\( \text{IsAnOrdRing}(R,A,M,r) \equiv \)
\( ( \text{IsAring}(R,A,M) \wedge (M \text{ is commutative on } R) \wedge \)
\( r\subseteq R\times R \wedge \text{IsLinOrder}(R,r) \wedge \)
\( (\forall a b.\ \forall c\in R.\ \langle a,b\rangle \in r \longrightarrow \langle A\langle a,c\rangle ,A\langle b,c\rangle \rangle \in r) \wedge \)
\( ( \text{Nonnegative}(R,A,r) \text{ is closed under } M)) \)
Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma (in reals) rchain_concat_weight:
assumes \( w:X\times X\rightarrow \mathbb{R} \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \), \( c_1\in \text{Chains}(X,n_1,x,y) \), \( c_2\in \text{Chains}(X,n_2,y,z) \) and \( n_1\in nat \), \( n_2\in nat \)
shows \( \text{RChainWeight}(w, \text{Concat}(c_1,c_2)) = \text{RChainWeight}(w,c_1) + \text{RChainWeight}(w,c_2) \) lemma concat_chains:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x_1,y_1) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,x_2,y_2) \)
defines \( c_3 \equiv \text{Concat}(c_1,c_2) \)
shows \( c_3 \in \text{Chains}(X,n_1 + n_2 + 1,x_1,y_2) \), \( \text{ChainLinks}(c_3): (n_1 + n_2 + 1)\rightarrow X\times X \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle c_1(n_1),c_2(0)\rangle ), \text{ChainLinks}(c_2)) \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle y_1,x_2\rangle ), \text{ChainLinks}(c_2)) \) lemma (in reals) nneg_has_nneg_inf:
assumes \( A\neq \emptyset \), \( A\subseteq \mathbb{R} ^+ \)
shows \( A \text{ has an infimum } \) and \( inf(A) \in \mathbb{R} ^+ \) lemma inf_incl_mono:
assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( \text{HasAnInfimum}(r,B) \), \( A\subseteq B \)
shows \( \langle \text{Infimum}(r,B), \text{Infimum}(r,A)\rangle \in r \) corollary (in reals) nonneg_inf_sum_inf:
assumes \( A\neq \emptyset \), \( A\subseteq \mathbb{R} ^+ \), \( B\neq \emptyset \), \( B\subseteq \mathbb{R} ^+ \)
shows \( \{x + y.\ \langle x,y\rangle \in A\times B\} \text{ has an infimum } \) and \( inf(A) + inf(B) = inf(\{x + y.\ \langle x,y\rangle \in A\times B\}) \) lemma chains_nempty:
assumes \( x\in X \) and \( y\in X \)
shows \( \{\langle 0,x\rangle ,\langle 1,y\rangle \} \in \text{Chains}(X,1,x,y) \), \( \{\langle 0,x\rangle ,\langle 1,y\rangle \}(0) = x \), \( \{\langle 0,x\rangle ,\langle 1,y\rangle \}(1) = y \), \( (\bigcup n\in nat\setminus \{0\}.\ \text{Chains}(X,n,x,y)) \neq \emptyset \) lemma (in monoid1) weight_one_link:
assumes \( x\in X \), \( y\in X \), \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w,\{\langle 0,x\rangle ,\langle 1,y\rangle \}) = w\langle x,y\rangle \) lemma (in loop1) zero_subset_nneg:
assumes \( B\subseteq L^+ \), \( 0 \in B \)
shows \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) = 0 \) and \( \text{HasAnInfimum}(r,B) \), \( \text{Infimum}(r,B) = 0 \) lemma (in reals) basic_props: shows \( ROrd \text{ is total on } \mathbb{R} \) and \( Add \text{ is commutative on } \mathbb{R} \)
corollary (in monoid1) weight_set_rev_eq:
assumes \( f \text{ is commutative on } G \), \( w:X\times X\rightarrow G \), \( \forall x\in X.\ \forall y\in X.\ w\langle x,y\rangle = w\langle y,x\rangle \)
shows \( \{ \text{ChainWeight}(w,c).\ c\in (\bigcup n\in nat\setminus \{0\}.\ \text{Chains}(X,n,x,y))\} = \) \( \{ \text{ChainWeight}(w,c).\ c\in (\bigcup n\in nat\setminus \{0\}.\ \text{Chains}(X,n,y,x))\} \) 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 (in reals) chain_dist_nneg:
assumes \( x\in X \), \( y\in X \) and \( w:X\times X\rightarrow \mathbb{R} ^+ \)
shows \( \text{ChainDist}(X,w,x,y) \in \mathbb{R} ^+ \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \) lemma (in reals) chain_dist_self_zero:
assumes \( x\in X \), \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( w\langle x,x\rangle = 0 \)
shows \( \text{ChainDist}(X,w,x,x) = 0 \) lemma (in reals) chain_dist_symm:
assumes \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( \forall x\in X.\ \forall y\in X.\ w\langle x,y\rangle = w\langle y,x\rangle \)
shows \( \text{ChainDist}(X,w,x,y) = \text{ChainDist}(X,w,y,x) \) lemma (in reals) chain_dist_tr_ineq:
assumes \( x\in X \), \( y\in X \), \( z\in X \) and \( w:X\times X\rightarrow \mathbb{R} ^+ \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \)
shows \( \text{ChainDist}(X,w,x,z) \leq \text{ChainDist}(X,w,x,y) + \text{ChainDist}(X,w,y,z) \)Definition of ChainWeightPMetric:
\( \text{ChainWeightPMetric}(X,w) \equiv \{\langle p, \text{ChainDist}(X,w,\text{fst}(p),\text{snd}(p))\rangle .\ p \in X\times X\} \)
Definition of IsApseudoMetric:
\( \text{IsApseudoMetric}(d,X,G,A,r) \equiv d:X\times X \rightarrow \text{Nonnegative}(G,A,r) \)
\( \wedge (\forall x\in X.\ d\langle x,x\rangle = \text{ TheNeutralElement}(G,A))\)
\( \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = d\langle y,x\rangle )\)
\( \wedge (\forall x\in X.\ \forall y\in X.\ \forall z\in X.\ \langle d\langle x,z\rangle , A\langle d\langle x,y\rangle ,d\langle y,z\rangle \rangle \rangle \in r) \)
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 }( \frac{1}{2} )^{\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
