map_ne

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometry.map_ne

English

The distance between two points is preserved by an affine isometry.

Русский

Расстояние между двумя точками сохраняется аффинной изометрией.

LaTeX

$$$d(f(x), f(y)) = d(x, y)$$$

Lean4

theorem map_ne {x y : P₁'} (h : x ≠ y) : f₁ x ≠ f₁ y :=
  f₁.injective.ne h

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

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

Разделы

Аффилиация

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