Mathlib.Topology.MetricSpace.Defs

MetricSpace structure

(α : Type u) : Type u extends PseudoMetricSpace α

Full source

/-- A metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This eg ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance]. -/
class MetricSpace (α : Type u) : Type u extends PseudoMetricSpace α where
  eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y

Metric Space

Informal description

A metric space is a type $\alpha$ equipped with a distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ satisfying the following properties: 1. Non-degeneracy: $\text{dist}(x, y) = 0$ if and only if $x = y$. 2. Symmetry: $\text{dist}(x, y) = \text{dist}(y, x)$ for all $x, y \in \alpha$. 3. Triangle inequality: $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$ for all $x, y, z \in \alpha$. The topology and uniformity on $\alpha$ are derived from the distance function, ensuring compatibility with the metric structure.

MetricSpace.ext theorem

{α : Type*} {m m' : MetricSpace α} (h : m.toDist = m'.toDist) : m = m'

Full source

/-- Two metric space structures with the same distance coincide. -/
@[ext]
theorem MetricSpace.ext {α : Type*} {m m' : MetricSpace α} (h : m.toDist = m'.toDist) :
    m = m' := by
  cases m; cases m'; congr; ext1; assumption

Uniqueness of Metric Space Structure via Distance Function

Informal description

Let $\alpha$ be a type, and let $m$ and $m'$ be two metric space structures on $\alpha$. If the distance functions associated with $m$ and $m'$ are equal, i.e., $m.\text{toDist} = m'.\text{toDist}$, then the metric space structures $m$ and $m'$ are identical.

MetricSpace.ofDistTopology definition

 {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0)
  (dist_comm : ∀ x y : α, dist x y = dist y x) (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
  (H : ∀ s : Set α, IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s)
  (eq_of_dist_eq_zero : ∀ x y : α, dist x y = 0 → x = y) : MetricSpace α

Full source

/-- Construct a metric space structure whose underlying topological space structure
(definitionally) agrees which a pre-existing topology which is compatible with a given distance
function. -/
def MetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ)
    (dist_self : ∀ x : α, dist x x = 0) (dist_comm : ∀ x y : α, dist x y = dist y x)
    (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
    (H : ∀ s : Set α, IsOpenIsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s)
    (eq_of_dist_eq_zero : ∀ x y : α, dist x y = 0 → x = y) : MetricSpace α :=
  { PseudoMetricSpace.ofDistTopology dist dist_self dist_comm dist_triangle H with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero _ _ }

Metric space construction from a distance function compatible with a given topology

Informal description

Given a type $\alpha$ with a topological space structure and a distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ satisfying: 1. Reflexivity: $\text{dist}(x, x) = 0$ for all $x \in \alpha$, 2. Symmetry: $\text{dist}(x, y) = \text{dist}(y, x)$ for all $x, y \in \alpha$, 3. Triangle inequality: $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$ for all $x, y, z \in \alpha$, 4. The topology is induced by the distance function (i.e., a set $s \subseteq \alpha$ is open if and only if for every $x \in s$ there exists $\epsilon > 0$ such that the ball $\{y \mid \text{dist}(x, y) < \epsilon\}$ is contained in $s$), 5. Non-degeneracy: $\text{dist}(x, y) = 0$ implies $x = y$ for all $x, y \in \alpha$, this constructs a metric space structure on $\alpha$ whose underlying topology agrees with the given one.

dist_eq_zero theorem

{x y : γ} : dist x y = 0 ↔ x = y

Full source

@[simp]
theorem dist_eq_zero {x y : γ} : distdist x y = 0 ↔ x = y :=
  Iff.intro eq_of_dist_eq_zero fun this => this ▸ dist_self _

Distance Vanishes if and only if Points are Equal

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the distance between them is zero if and only if $x = y$, i.e., $\text{dist}(x, y) = 0 \leftrightarrow x = y$.

zero_eq_dist theorem

{x y : γ} : 0 = dist x y ↔ x = y

Full source

@[simp]
theorem zero_eq_dist {x y : γ} : 0 = dist x y ↔ x = y := by rw [eq_comm, dist_eq_zero]

Zero Equals Distance if and only if Points are Equal

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the equality $0 = \text{dist}(x, y)$ holds if and only if $x = y$.

dist_ne_zero theorem

{x y : γ} : dist x y ≠ 0 ↔ x ≠ y

Full source

theorem dist_ne_zero {x y : γ} : distdist x y ≠ 0dist x y ≠ 0 ↔ x ≠ y := by
  simpa only [not_iff_not] using dist_eq_zero

Nonzero Distance Characterizes Distinct Points in Metric Space

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the distance between them is nonzero if and only if $x \neq y$, i.e., $\text{dist}(x, y) \neq 0 \leftrightarrow x \neq y$.

dist_le_zero theorem

{x y : γ} : dist x y ≤ 0 ↔ x = y

Full source

@[simp]
theorem dist_le_zero {x y : γ} : distdist x y ≤ 0 ↔ x = y := by
  simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y

Distance Non-Positive if and only if Points are Equal

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the distance between them is less than or equal to zero if and only if $x = y$, i.e., $\text{dist}(x, y) \leq 0 \leftrightarrow x = y$.

dist_pos theorem

{x y : γ} : 0 < dist x y ↔ x ≠ y

Full source

@[simp]
theorem dist_pos {x y : γ} : 0 < dist x y ↔ x ≠ y := by
  simpa only [not_le] using not_congr dist_le_zero

Positivity of Distance Characterizes Distinct Points in Metric Space

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the distance between them is strictly positive if and only if $x \neq y$, i.e., $\text{dist}(x, y) > 0 \leftrightarrow x \neq y$.

nndist_eq_zero theorem

{x y : γ} : nndist x y = 0 ↔ x = y

Full source

/-- Characterize the equality of points as the vanishing of the nonnegative distance -/
@[simp]
theorem nndist_eq_zero {x y : γ} : nndistnndist x y = 0 ↔ x = y := by
  simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]

Vanishing Distance Characterizes Equality in Metric Spaces

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the non-negative distance $\text{nndist}(x, y)$ equals zero if and only if $x = y$.

zero_eq_nndist theorem

{x y : γ} : 0 = nndist x y ↔ x = y

Full source

@[simp]
theorem zero_eq_nndist {x y : γ} : 0 = nndist x y ↔ x = y := by
  simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, zero_eq_dist]

Zero Distance Equivalence in Metric Spaces

Informal description

For any two points $x$ and $y$ in a metric space $\gamma$, the non-negative distance between them is zero if and only if $x = y$, i.e., $0 = \text{nndist}(x, y) \leftrightarrow x = y$.

Metric.closedBall_zero theorem

: closedBall x 0 = { x }

Full source

@[simp] theorem closedBall_zero : closedBall x 0 = {x} := Set.ext fun _ => dist_le_zero

Zero-Radius Closed Ball is Singleton

Informal description

For any point $x$ in a metric space $\gamma$, the closed ball centered at $x$ with radius $0$ is equal to the singleton set $\{x\}$, i.e., $\overline{B}(x, 0) = \{x\}$.

Metric.sphere_zero theorem

: sphere x 0 = { x }

Full source

@[simp] theorem sphere_zero : sphere x 0 = {x} := Set.ext fun _ => dist_eq_zero

Zero-Radius Sphere is Singleton

Informal description

For any point $x$ in a metric space $\gamma$, the sphere centered at $x$ with radius $0$ is equal to the singleton set $\{x\}$, i.e., $\text{sphere}(x, 0) = \{x\}$.

Metric.subsingleton_closedBall theorem

(x : γ) {r : ℝ} (hr : r ≤ 0) : (closedBall x r).Subsingleton

Full source

theorem subsingleton_closedBall (x : γ) {r : ℝ} (hr : r ≤ 0) : (closedBall x r).Subsingleton := by
  rcases hr.lt_or_eq with (hr | rfl)
  · rw [closedBall_eq_empty.2 hr]
    exact subsingleton_empty
  · rw [closedBall_zero]
    exact subsingleton_singleton

Closed Balls with Non-Positive Radius are Subsingletons

Informal description

For any point $x$ in a metric space $\gamma$ and any non-positive real number $r \leq 0$, the closed ball $\overline{B}(x, r)$ is a subsingleton set (i.e., contains at most one point).

Metric.subsingleton_sphere theorem

(x : γ) {r : ℝ} (hr : r ≤ 0) : (sphere x r).Subsingleton

Full source

theorem subsingleton_sphere (x : γ) {r : ℝ} (hr : r ≤ 0) : (sphere x r).Subsingleton :=
  (subsingleton_closedBall x hr).anti sphere_subset_closedBall

Spheres with Non-Positive Radius are Subsingletons

Informal description

For any point $x$ in a metric space $\gamma$ and any non-positive real number $r \leq 0$, the sphere $\{ y \in \gamma \mid \text{dist}(y, x) = r \}$ is a subsingleton set (i.e., contains at most one point).

MetricSpace.replaceUniformity abbrev

 {γ} [U : UniformSpace γ] (m : MetricSpace γ) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : MetricSpace γ

Full source

/-- Build a new metric space from an old one where the bundled uniform structure is provably
(but typically non-definitionaly) equal to some given uniform structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev MetricSpace.replaceUniformity {γ} [U : UniformSpace γ] (m : MetricSpace γ)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : MetricSpace γ where
  toPseudoMetricSpace := PseudoMetricSpace.replaceUniformity m.toPseudoMetricSpace H
  eq_of_dist_eq_zero := @eq_of_dist_eq_zero _ _

Metric Space Construction from Uniformity Compatibility

Informal description

Given a uniform space $\gamma$ with uniform structure $U$ and a metric space structure $m$ on $\gamma$, if the uniformity filter $\mathfrak{U}(U)$ coincides with the uniformity induced by the metric space $m$, then there exists a metric space structure on $\gamma$ that is compatible with $U$.

MetricSpace.replaceUniformity_eq theorem

 {γ} [U : UniformSpace γ] (m : MetricSpace γ) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) :
  m.replaceUniformity H = m

Full source

theorem MetricSpace.replaceUniformity_eq {γ} [U : UniformSpace γ] (m : MetricSpace γ)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m := by
  ext; rfl

Metric Space Uniformity Replacement Preserves Structure

Informal description

Let $\gamma$ be a uniform space with uniform structure $U$, and let $m$ be a metric space structure on $\gamma$. If the uniformity filter $\mathfrak{U}(U)$ coincides with the uniformity induced by the metric space $m$, then the metric space structure obtained by replacing the uniformity of $m$ with $U$ is equal to $m$ itself.

MetricSpace.replaceTopology abbrev

 {γ} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) :
  MetricSpace γ

Full source

/-- Build a new metric space from an old one where the bundled topological structure is provably
(but typically non-definitionaly) equal to some given topological structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev MetricSpace.replaceTopology {γ} [U : TopologicalSpace γ] (m : MetricSpace γ)
    (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) : MetricSpace γ :=
  @MetricSpace.replaceUniformity γ (m.toUniformSpace.replaceTopology H) m rfl

Metric Space Construction with Prescribed Topology

Informal description

Given a topological space $\gamma$ with topology $U$ and a metric space structure $m$ on $\gamma$, if $U$ coincides with the topology induced by the metric space $m$, then there exists a metric space structure on $\gamma$ that is compatible with $U$.

MetricSpace.replaceTopology_eq theorem

 {γ} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) :
  m.replaceTopology H = m

Full source

theorem MetricSpace.replaceTopology_eq {γ} [U : TopologicalSpace γ] (m : MetricSpace γ)
    (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) :
    m.replaceTopology H = m := by
  ext; rfl

Metric Space Topology Replacement Preserves Structure

Informal description

Let $\gamma$ be a topological space with topology $U$, and let $m$ be a metric space structure on $\gamma$. If $U$ is equal to the topology induced by the metric space $m$, then the metric space structure obtained by replacing the topology of $m$ with $U$ is equal to $m$ itself.

MetricSpace.replaceBornology abbrev

 {α} [B : Bornology α] (m : MetricSpace α) (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
  MetricSpace α

Full source

/-- Build a new metric space from an old one where the bundled bornology structure is provably
(but typically non-definitionaly) equal to some given bornology structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev MetricSpace.replaceBornology {α} [B : Bornology α] (m : MetricSpace α)
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : MetricSpace α :=
  { PseudoMetricSpace.replaceBornology _ H, m with toBornology := B }

Metric Space Construction with Prescribed Bornology

Informal description

Given a metric space $(α, d)$ and a bornology $B$ on $α$ such that for every subset $s \subseteq α$, $s$ is bounded with respect to $B$ if and only if $s$ is bounded with respect to the bornology induced by the metric $d$, then there exists a metric space structure on $α$ where the bornology is (non-definitionally) equal to $B$.

MetricSpace.replaceBornology_eq theorem

 {α} [m : MetricSpace α] [B : Bornology α] (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
  MetricSpace.replaceBornology _ H = m

Full source

theorem MetricSpace.replaceBornology_eq {α} [m : MetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    MetricSpace.replaceBornology _ H = m := by
  ext
  rfl

Equality of Metric Space Structures with Prescribed Bornology

Informal description

Let $\alpha$ be a type equipped with a metric space structure $m$ and a bornology $B$. If for every subset $s \subseteq \alpha$, $s$ is bounded with respect to $B$ if and only if $s$ is bounded with respect to the bornology induced by the metric space structure $m$, then the metric space structure obtained by replacing the bornology of $m$ with $B$ is equal to $m$.

instMetricSpaceEmpty instance

: MetricSpace Empty

Full source

instance : MetricSpace Empty where
  dist _ _ := 0
  dist_self _ := rfl
  dist_comm _ _ := rfl
  edist _ _ := 0
  eq_of_dist_eq_zero _ := Subsingleton.elim _ _
  dist_triangle _ _ _ := show (0 : ℝ) ≤ 0 + 0 by rw [add_zero]
  toUniformSpace := inferInstance
  uniformity_dist := Subsingleton.elim _ _

Metric Space Structure on the Empty Set

Informal description

The empty set $\emptyset$ is equipped with the canonical metric space structure, where the distance function is trivial since there are no elements to compare.

instMetricSpacePUnit instance

: MetricSpace PUnit.{u + 1}

Full source

instance : MetricSpace PUnitPUnit.{u + 1} where
  dist _ _ := 0
  dist_self _ := rfl
  dist_comm _ _ := rfl
  edist _ _ := 0
  eq_of_dist_eq_zero _ := Subsingleton.elim _ _
  dist_triangle _ _ _ := show (0 : ℝ) ≤ 0 + 0 by rw [add_zero]
  toUniformSpace := inferInstance
  uniformity_dist := by
    simp +contextual [principal_univ, eq_top_of_neBot (𝓤 PUnit)]

Metric Space Structure on the Singleton Type

Informal description

The singleton type `PUnit` is equipped with the canonical metric space structure.

instDistAdditive instance

: Dist (Additive X)

Full source

instance : Dist (Additive X) := ‹Dist X›

Distance Function on Additive Type

Informal description

The additive version of a type $X$ inherits the distance function from $X$. That is, for any $a, b \in X$, the distance between their additive counterparts $\text{ofMul}(a)$ and $\text{ofMul}(b)$ in $\text{Additive}(X)$ is equal to the distance between $a$ and $b$ in $X$.

instDistMultiplicative instance

: Dist (Multiplicative X)

Full source

instance : Dist (Multiplicative X) := ‹Dist X›

Distance on Multiplicative Type

Informal description

For any type `X` equipped with a distance function, the multiplicative version of `X` (denoted `Multiplicative X`) inherits the same distance function. Specifically, the distance between two elements `ofMul a` and `ofMul b` in `Multiplicative X` is equal to the distance between `a` and `b` in `X`.

dist_ofMul theorem

(a b : X) : dist (ofMul a) (ofMul b) = dist a b

Full source

@[simp] theorem dist_ofMul (a b : X) : dist (ofMul a) (ofMul b) = dist a b := rfl

Distance Preservation under `ofMul` Map

Informal description

For any two elements $a$ and $b$ of a type $X$ equipped with a distance function, the distance between their images under the `ofMul` map in the additive version of $X$ is equal to the distance between $a$ and $b$ in $X$. That is, $\text{dist}(\text{ofMul}(a), \text{ofMul}(b)) = \text{dist}(a, b)$.

dist_ofAdd theorem

(a b : X) : dist (ofAdd a) (ofAdd b) = dist a b

Full source

@[simp] theorem dist_ofAdd (a b : X) : dist (ofAdd a) (ofAdd b) = dist a b := rfl

Distance Preservation under `ofAdd` Map in Multiplicative Type

Informal description

For any two elements $a$ and $b$ of a type $X$ equipped with a distance function, the distance between their images under the `ofAdd` map in the multiplicative version of $X$ is equal to the distance between $a$ and $b$ in $X$. That is, $\text{dist}(\text{ofAdd}(a), \text{ofAdd}(b)) = \text{dist}(a, b)$.

dist_toMul theorem

(a b : Additive X) : dist a.toMul b.toMul = dist a b

Full source

@[simp] theorem dist_toMul (a b : Additive X) : dist a.toMul b.toMul = dist a b := rfl

Distance Preservation under $\text{toMul}$ Map in Additive Type

Informal description

For any two elements $a$ and $b$ in the additive type $\text{Additive}\, X$, the distance between their images under the $\text{toMul}$ map is equal to the distance between $a$ and $b$ in $\text{Additive}\, X$. That is, $\text{dist}(a.\text{toMul}, b.\text{toMul}) = \text{dist}(a, b)$.

dist_toAdd theorem

(a b : Multiplicative X) : dist a.toAdd b.toAdd = dist a b

Full source

@[simp] theorem dist_toAdd (a b : Multiplicative X) : dist a.toAdd b.toAdd = dist a b := rfl

Distance Preservation under `toAdd` Map in Multiplicative Type

Informal description

For any two elements $a$ and $b$ in the multiplicative type `Multiplicative X`, the distance between their images under the `toAdd` map is equal to the distance between $a$ and $b$ in `Multiplicative X$. That is, $\text{dist}(a.\text{toAdd}, b.\text{toAdd}) = \text{dist}(a, b)$.

instMetricSpaceAdditive instance

[MetricSpace X] : MetricSpace (Additive X)

Full source

instance [MetricSpace X] : MetricSpace (Additive X) := ‹MetricSpace X›

Metric Space Structure on Additive Types

Informal description

For any metric space $X$, the additive version $\text{Additive}\, X$ inherits a metric space structure where the distance function remains unchanged.

instMetricSpaceMultiplicative instance

[MetricSpace X] : MetricSpace (Multiplicative X)

Full source

instance [MetricSpace X] : MetricSpace (Multiplicative X) := ‹MetricSpace X›

Metric Space Structure on Multiplicative Type Synonyms

Informal description

For any metric space $X$, the multiplicative type synonym $\text{Multiplicative}\, X$ inherits a metric space structure from $X$, where the distance function remains unchanged.

instDistOrderDual instance

: Dist Xᵒᵈ

Full source

instance : Dist Xᵒᵈ := ‹Dist X›

Distance Function on Order Dual

Informal description

The order dual $X^{\text{op}}$ of a type $X$ with a distance function inherits the same distance function, where the distance between two elements in the dual is equal to their distance in the original type.

dist_toDual theorem

(a b : X) : dist (toDual a) (toDual b) = dist a b

Full source

@[simp] theorem dist_toDual (a b : X) : dist (toDual a) (toDual b) = dist a b := rfl

Distance Preservation under Order Dual Map: $\text{dist}(\text{toDual}(a), \text{toDual}(b)) = \text{dist}(a, b)$

Informal description

For any two elements $a$ and $b$ in a metric space $X$, the distance between their images under the order dual map $\text{toDual} : X \to X^{\text{op}}$ is equal to their original distance, i.e., $\text{dist}(\text{toDual}(a), \text{toDual}(b)) = \text{dist}(a, b)$.

dist_ofDual theorem

(a b : Xᵒᵈ) : dist (ofDual a) (ofDual b) = dist a b

Full source

@[simp] theorem dist_ofDual (a b : Xᵒᵈ) : dist (ofDual a) (ofDual b) = dist a b := rfl

Distance Preservation under Inverse Order Dual Map: $\text{dist}(\text{ofDual}(a), \text{ofDual}(b)) = \text{dist}(a, b)$

Informal description

For any two elements $a$ and $b$ in the order dual $X^{\text{op}}$ of a metric space $X$, the distance between their images under the inverse order dual map $\text{ofDual} : X^{\text{op}} \to X$ is equal to their original distance, i.e., $\text{dist}(\text{ofDual}(a), \text{ofDual}(b)) = \text{dist}(a, b)$.

instMetricSpaceOrderDual instance

[MetricSpace X] : MetricSpace Xᵒᵈ

Full source

instance [MetricSpace X] : MetricSpace Xᵒᵈ := ‹MetricSpace X›

Metric Space Structure on Order Duals

Informal description

For any metric space $X$, the order dual $X^{\text{op}}$ is also a metric space with the same distance function.

Mathlib.Topology.MetricSpace.Defs

Implementation notes

Tags