edist_eq

Mathlib.Topology.MetricSpace.Completion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.edist_eq

English

Same as edist_eq: edist between images from α to Completion α equals the original edist.

Русский

То же, что и edist_eq: edist между образами из α в Completion α равен исходному edist.

LaTeX

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

Lean4

@[simp]
protected theorem edist_eq (x y : α) : edist (x : Completion α) y = edist x y :=
  coe_isometry x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru