coe_isometry — Mathlib

English

For all x,y in α, edist (x : Completion α) y = edist x y; i.e., the embedding is an isometry for the extended metric.

Русский

Для любых x,y ∈ α выполняется edist (x в Completion α) y = edist x y; вложение является изометрией для расширенной метрики.

LaTeX

$$$\operatorname{edist}(x:\mathrm{Completion}\,\alpha, y) = \operatorname{edist}(x,y)$$$

Lean4

/-- The embedding of a metric space in its completion is an isometry. -/
theorem coe_isometry : Isometry ((↑) : α → Completion α) :=
  Isometry.of_dist_eq Completion.dist_eq

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