toEMetricSpace — Mathlib

English

A metric space naturally carries an emetric structure; the edistance is defined as the real-valued distance, and the uniformities align.

Русский

Метрическое пространство естественно обладает структурой эметрического пространства; edist задаётся через обычное расстояние, униформности согласованы.

LaTeX

$$$ \text{MetricSpace } \gamma \Rightarrow \text{EMetricSpace } \gamma$$$

Lean4

/-- A metric space induces an emetric space -/
instance (priority := 100) _root_.MetricSpace.toEMetricSpace : EMetricSpace γ :=
  .ofT0PseudoEMetricSpace γ

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