nndist_eq

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#IsometryClass.nndist_eq

English

Distances measured in the normed sense are preserved by an isometry: nndist(f(x), f(y)) = nndist(x, y).

Русский

Расстояния в нормированном смысле сохраняются изометрией: nndist(f(x), f(y)) = nndist(x, y).

LaTeX

$$$ \operatorname{nndist}(f(x), f(y)) = \operatorname{nndist}(x, y). $$$

Lean4

protected theorem nndist_eq (x y : α) : nndist (f x) (f y) = nndist x y :=
  (IsometryClass.isometry f).nndist_eq x y

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

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

Разделы

Аффилиация

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