metricSpace — Mathlib

English

There is a metric space structure on e.finiteSubspace compatible with the emetric.

Русский

На e.finiteSubspace задана структура метрического пространства, совместимая с эмежитикой.

LaTeX

$$instance metricSpace : MetricSpace e.finiteSubspace := ...$$

Lean4

/-- Metric space structure on `e.finiteSubspace`. We use `EMetricSpace.toMetricSpace`
to ensure that this definition agrees with `e.emetricSpace`. -/
instance metricSpace : MetricSpace e.finiteSubspace :=
  by
  letI := e.emetricSpace
  refine EMetricSpace.toMetricSpace fun x y => ?_
  change e (x - y) ≠ ⊤
  exact ne_top_of_le_ne_top (ENNReal.add_lt_top.2 ⟨x.2, y.2⟩).ne (e.map_sub_le x y)

Похожие утверждения