dist_mk — Mathlib

English

The separation quotient of a metric space α is itself a metric space, and the distance between mk p and mk q is the distance between representatives p and q: dist(mk p, mk q) = dist(p,q).

Русский

Разделяющее отношение в метрическом пространстве α образует метричеcкое пространство; расстояние междуmk p и mk q равно расстоянию между представителями p и q: dist(mk p, mk q) = dist(p,q).

LaTeX

$$$\\operatorname{dist}_{\\mathrm{SeparationQuotient}(α)}(\\mathrm{mk}(p),\\mathrm{mk}(q))=\\operatorname{dist}_α(p,q)$$$

Lean4

theorem dist_mk {α : Type u} [PseudoMetricSpace α] (p q : α) : dist (mk p) (mk q) = dist p q :=
  rfl

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