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.

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:

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 *disk*s from *pmetric_space*
are now called *ball*s in *pmetric_space1*. The notation for right and left division from
*pmetric_space1* is not used in *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:

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.

proof

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:

The collection of open disks (caled *ball*s in the *pmetric_space1* context
is a base for the (real valued) metric topology.

** theorem ** **(in** pmetric_space1**)** rdisks_are_base:

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

** theorem ** **(in** pmetric_space1**)** rmetric_top_carrier:

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

** theorem ** **(in** metric_space1**)** rmetric_space_T2:

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

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

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

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

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