IsarMathLib

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

theory MetricSpace_ZF_1 imports Real_ZF_2

begin

The development of metric spaces in IsarMathLib is different from the usual treatment of the subject because the notion of a metric (or a pseudometric) is defined in the MetricSpace_ZF theory a more generally as a function valued in an ordered loop. This theory file brings the subject closer to the standard way by specializing that general definition to the usual special case where the value of the metric are nonnegative real numbers.

Real valued metric scapes: context and notation

The reals context (locale) defined in the Real_ZF_2 theory fixes a model of reals (i.e. a complete ordered field) and defines notation for things like zero, one, the set of positive numbers, absolute value etc. For metric spaces we reuse the notation defined there.

The rpmetric_space locale extends the reals locale, adding the carrier \(X\) of the metric space and the metric \(\mathcal{d}\) to the context, together with the assumption that \(\mathcal{d}:X\times X \rightarrow \mathbb{R}^+\) is a pseudo metric. We choose to denote the disk in \(X\) with center \(c\) and radius \(r\) as \( ball(c,r) \) As in the pmetric_space locale we define the \(\tau\) to be the metric topology, i.e. the topology induced by the (real valued) pseudometric \(\mathcal{d}\). An alternative would be to define the rpmetric_space as an extension of the rpmetric_space context, but that is in turn an extension of the loop1 locale that defines notation for left and right division which which do not want in the context of real numbers.

locale rpmetric_space = reals +

assumes pmetricAssum: \( \text{IsApseudoMetric}(\mathcal{d} ,X,\mathbb{R} ,Add,ROrd) \)

defines \( ball(c,r) \equiv \text{Disk}(X,\mathcal{d} ,ROrd,c,r) \)

defines \( \tau \equiv \text{MetricTopology}(X,\mathbb{R} ,Add,ROrd,\mathcal{d} ) \)

defines \( int(D) \equiv \text{Interior}(D,\tau ) \)

defines \( cl(D) \equiv \text{Closure}(D,\tau ) \)

The propositions proven in the pmetric_space context defined in Metric_Space_ZF theory are valid in the rpmetric_space context.

lemma (in rpmetric_space) pmetric_space_rpmetric_space_valid:

shows \( pmetric\_space(\mathbb{R} ,Add,ROrd,\mathcal{d} ,X) \) unfolding pmetric_space_def, pmetric_space_axioms_def, loop1_def using pmetricAssum, reals_loop

The context rpmetric_space is a special case of context pmetric_space where the fixed objects in pmetric_space map to (in the order defined in pmetric_space) the set of real numbers, real addition, the order relation on reals, the strict order relation on reals, the set of non-negative reals and the set of positive reals. The metrics \(d\) maps to the real metrics \( \mathcal{d} \), the carrier of the metric space \(X\) is still \(X\), and the disks from pmetric_space are now called balls in rpmetric_space. The notation for right and left division from rpmetric_space is not used in pmetric_space.

sublocale rpmetric_space < pmetric_space

using pmetric_space_rpmetric_space_valid

The rmetric_space locale (context) specializes the the rpmetric_space context by adding the assumption of identity of indiscernibles.

locale rmetric_space = rpmetric_space +

assumes ident_indisc: \( \forall x\in X.\ \forall y\in Y.\ \mathcal{d} \langle x,y\rangle = 0 \longrightarrow x=y \)

The propositions proven in the metric_space context defined in Metric_Space_ZF theory are valid in the rmetric_space context.

lemma (in rmetric_space) metric_space_rmetric_space_valid:

shows \( metric\_space(\mathbb{R} ,Add,ROrd,\mathcal{d} ,X) \) unfolding metric_space_def, metric_space_axioms_def using pmetric_space_rpmetric_space_valid, ident_indisc

The rmetric_space context is a special case of the metric_space context, with fixed objects mapping the same as in the mapping between rpmetric_space and pmetric_space above.

sublocale rmetric_space < metric_space

proof

from ident_indisc show \( \forall x\in X.\ \forall y\in X.\ \mathcal{d} \langle x, y\rangle = \text{ TheNeutralElement}(\mathbb{R} , Add) \longrightarrow x = y \)

qed

Real valued metric spaces are Hausdorff as topological spaces

The usual (real-valued) metric spaces are a special case of ordered loop valued metric spaces defined in the MetricSpace_ZF theory, hence they are \(T_2\) as topological spaces. Below we repeat the major theorems of MetricSpace_ZF theory specialized the standard setting of real valued metrics.

Since in the rpmetric_space context \(\mathfrak{d}\) is a pseudometrics the (real valued) metric topology indeed a topology.

theorem (in rpmetric_space) rpmetric_is_top:

shows \( \tau \text{ is a topology } \) using rord_down_directs, pmetric_is_top

The collection of open disks (caled balls in the rpmetric_space context is a base for the (real valued) metric topology.

theorem (in rpmetric_space) rdisks_are_base:

shows \( (\bigcup c\in X.\ \{ball(c,R).\ R\in \mathbb{R} _+\}) \text{ is a base for } \tau \) using rord_down_directs, disks_are_base

\(X\) is the carrier of the (real valued) metric topology.

theorem (in rpmetric_space) rmetric_top_carrier:

shows \( \bigcup \tau = X \) using rord_down_directs, metric_top_carrier

The topology generated by a (real valued) metric is Hausdorff (i.e. \(T_2\)).

theorem (in rmetric_space) rmetric_space_T2:

shows \( \tau \text{ is }T_2 \) using rord_down_directs, metric_space_T2

Real valued (pseudo)metric spaces as uniform spaces

The ordered loop valued pseudometric spaces are uniform spaces. In this section we specialize major propositions from that context to the real valued pseudometric.

In the MetricSpace_ZF theory we define a property IsHalfable of an ordered loop that states that for every positive element \(b_1\) of the loop there is another (positive) one \(b_2\) such that \(b_2+b_2 \leq b_1\). This property is needed for the ordered loop valued pseudometric space to be a uniform space. In the next lemma we show that real numbers satisfy this property.

lemma (in reals) pos_reals_halfable:

shows \( \text{IsHalfable}(\mathbb{R} ,Add,ROrd) \)proof

{

fix \( x \)

assume \( x\in \mathbb{R} _+ \)

let \( y = ( 2 ^{-1})\cdot x \)

from \( x\in \mathbb{R} _+ \) have \( x\in \mathbb{R} \) and \( y\in \mathbb{R} _+ \) using element_pos, pos_mul_closed, ord_ring_less_members, one_half_pos(2)

from \( x\in \mathbb{R} \) have \( ( 2 ^{-1} + 2 ^{-1})\cdot x = x \) using half_half_one(2), Ring_ZF_1_L3(6)

with \( x\in \mathbb{R} \) have \( y + y \leq x \) using ord_ring_less_members, ring_oper_distr(2), one_half_pos(2), ring_ord_refl

with \( y\in \mathbb{R} _+ \) have \( \exists y\in \mathbb{R} _+.\ y + y \leq x \)

}

then show \( thesis \) unfolding IsHalfable_def

qed

In the rpmetric_space we will write \( \text{UniformGauge}(X,\mathbb{R} ,Add,ROrd,\mathcal{d} ) \) i.e. \(\{\mathcal{d}^{-1}([0,b]: b \in \mathbb{R}_+ \}\) as \(\mathfrak{U}\).

abbreviation (in rpmetric_space)

\( \mathfrak{U} \equiv \text{UniformGauge}(X,\mathbb{R} ,Add,ROrd,\mathcal{d} ) \)

\(\mathfrak{U}\) is a fundamental system of entourages, hence its supersets form a uniformity on \(X\) and hence those supersets define a topology on \(X\). This is a special case of the theorem metric_gauge_base from the Metric_Space_ZF theory but instead an ordered loop we have real numbers, so all the premises are automatically satisfied, except for the one of \(X\) being nonempty.

theorem (in rpmetric_space) metric_gauge_base:

assumes \( X\neq \emptyset \)

shows \( \mathfrak{U} \text{ is a uniform base on } X \), \( \text{Supersets}(X\times X,\mathfrak{U} ) \text{ is a uniformity on } X \), \( \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{U} ),X) \text{ is a topology } \), \( \bigcup \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{U} ),X) = X \) using assms, rord_down_directs, pos_non_empty, pos_reals_halfable, metric_gauge_base

The topology generated by open disks is the same as the one coming from the the unifomity consisting of supersets of sets in \(\mathfrak{U}\).

theorem (in rpmetric_space) rmetric_top_is_uniform_top:

assumes \( X\neq \emptyset \)

shows \( \tau = \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{U} ),X) \) using assms, rord_down_directs, pos_non_empty, pos_reals_halfable, metric_top_is_uniform_top

end

lemma (in reals) reals_loop: shows \( \text{IsAnOrdLoop}(\mathbb{R} ,Add,ROrd) \)

lemma (in rpmetric_space) pmetric_space_rpmetric_space_valid: shows \( pmetric\_space(\mathbb{R} ,Add,ROrd,\mathcal{d} ,X) \)

lemma (in reals) rord_down_directs: shows \( ROrd \text{ down-directs } \mathbb{R} _+ \)

theorem (in pmetric_space) pmetric_is_top:

assumes \( r \text{ down-directs } L_+ \)

shows \( \tau \text{ is a topology } \)

theorem (in pmetric_space) disks_are_base:

assumes \( r \text{ down-directs } L_+ \)

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ is a base for } \tau \)

theorem (in pmetric_space) metric_top_carrier:

assumes \( r \text{ down-directs } L_+ \)

shows \( \bigcup \tau = X \)

theorem (in metric_space) metric_space_T2:

assumes \( r \text{ down-directs } L_+ \)

shows \( \tau \text{ is }T_2 \)

lemma (in ring1) element_pos: shows \( a\in R_+ \longleftrightarrow 0 \lt a \)

lemma (in field1) pos_mul_closed:

assumes \( 0 \lt a \), \( 0 \lt b \)

shows \( 0 \lt a\cdot b \)

lemma (in ring1) ord_ring_less_members:

assumes \( a \lt b \)

shows \( a\in R \), \( b\in R \)

lemma (in field1) one_half_pos: shows \( 2 ^{-1} \in R_+ \), \( 0 \lt 2 ^{-1} \)

lemma (in field1) half_half_one: shows \( 2 ^{-1}\in R \), \( 2 ^{-1} + 2 ^{-1} = 1 \)

lemma (in ring0) Ring_ZF_1_L3:

assumes \( a\in R \)

shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \)

lemma (in ring0) ring_oper_distr:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \)

lemma (in ring1) ring_ord_refl:

assumes \( a\in R \)

shows \( a\leq a \)

Definition of IsHalfable: \( \text{IsHalfable}(L,A,r) \equiv \forall b_1\in \text{PositiveSet}(L,A,r).\ \exists b_2\in \text{PositiveSet}(L,A,r).\ \langle A\langle b_2,b_2\rangle ,b_1\rangle \in r \)

lemma (in reals) pos_non_empty: shows \( \mathbb{R} _+\neq 0 \)

lemma (in reals) pos_reals_halfable: shows \( \text{IsHalfable}(\mathbb{R} ,Add,ROrd) \)

theorem (in rpmetric_space) metric_gauge_base:

assumes \( X\neq \emptyset \)

theorem (in pmetric_space) metric_top_is_uniform_top:

assumes \( X\neq \emptyset \), \( L_+\neq \emptyset \), \( r \text{ down-directs } L_+ \), \( \text{IsHalfable}(L,A,r) \)

shows \( \tau = \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{B} ),X) \)