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 \(\mathfrak{d}\) to the context, together with the assumption that \(\mathfrak{d}:X\times X \rightarrow \mathbb{R}\) is a pseudo metric. 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}(\ \lt d>,X,\mathbb{R} ,Add,ROrd) \)

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

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,\ \lt d>,X) \) unfolding pmetric_space_def, pmetric_space_axioms_def, loop1_def using pmetricAssum, reals_loop

It is convenient to have the collection of all open balls in given (p) metrics defined as a separate notion.

definition (in pmetric_space1)

\( Open\_Balls \equiv \bigcup c\in X.\ \{ball(c,r).\ r \in \mathbb{R} _+\} \)

Topology on a metric space is defined as the collection of sets that are unions of open balls of the (p)metric.

definition (in pmetric_space1)

\( Metric\_Topology \equiv \{\bigcup A.\ A \in Pow(Open\_Balls)\} \)

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.\ \ \lt 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,\ \lt d>,X) \) unfolding metric_space_def, metric_space_axioms_def using pmetric_space_pmetric_space1_valid, ident_indisc

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.

Since in the pmetric_space1 context \(\mathfrak{d}\) is a pseudometrics the (p)metric topology as defined above is indeed a topology, the set of open balls is the base of that topology and the carrier of the topology is the underlying (p)metric space carrier \(X\).

theorem (in pmetric_space1) rpmetric_is_top:

shows \( Metric\_Topology \text{ is a topology } \), \( Open\_Balls \text{ is a base for } Metric\_Topology \), \( \bigcup Metric\_Topology = X \) unfolding Open_Balls_def, Metric_Topology_def using rord_down_directs, pmetric_space_pmetric_space1_valid, pmetric_is_top

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

theorem (in metric_space1) rmetric_space_T2:

shows \( Metric\_Topology \text{ is }T_2 \) unfolding Open_Balls_def, Metric_Topology_def using rord_down_directs, metric_space_metric_space1_valid, metric_space_T2

end

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

lemma (in pmetric_space1) pmetric_space_pmetric_space1_valid: shows \( pmetric\_space(\mathbb{R} ,Add,ROrd,\ \lt d>,X) \)

Definition of Open_Balls: \( Open\_Balls \equiv \bigcup c\in X.\ \{ball(c,r).\ r \in \mathbb{R} _+\} \)

Definition of Metric_Topology: \( Metric\_Topology \equiv \{\bigcup A.\ A \in Pow(Open\_Balls)\} \)

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_+ \)

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

defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)

shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)

lemma (in metric_space1) metric_space_metric_space1_valid: shows \( metric\_space(\mathbb{R} ,Add,ROrd,\ \lt d>,X) \)