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.

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 pmetric_space1 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 pmetric_space1 as an extension of the pmetric_space1 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 pmetric_space1 = 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 pmetric_space1 context.

lemma (in pmetric_space1) pmetric_space_pmetric_space1_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 pmetric_space1 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 pmetric_space1. The notation for right and left division from pmetric_space1 is not used in pmetric_space.

sublocale pmetric_space1 < pmetric_space

using pmetric_space_pmetric_space1_valid

The metric_space1 locale (context) specializes the the pmetric_space1 context by adding the assumption of identity of indiscernibles.

locale metric_space1 = pmetric_space1 +

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 metric_space1 context.

lemma (in metric_space1) metric_space_metric_space1_valid:

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

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

sublocale metric_space1 < 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

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 pmetric_space1 context \(\mathfrak{d}\) is a pseudometrics the (real valued) metric topology indeed a topology.

theorem (in pmetric_space1) 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 pmetric_space1 context is a base for the (real valued) metric topology.

theorem (in pmetric_space1) 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 pmetric_space1) 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 metric_space1) rmetric_space_T2:

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