isometry

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.isometry

English

A linear isometry preserves distances: for all x, y, d(f(x), f(y)) = d(x, y).

Русский

Линейная изометрия сохраняет расстояния: для всех x, y выполняется d(f(x), f(y)) = d(x, y).

LaTeX

$$$d\bigl(f(x), f(y)\bigr) = d(x, y)$$$

Lean4

protected theorem isometry : Isometry f :=
  AddMonoidHomClass.isometry_of_norm f.toLinearMap (norm_map _)

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

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

Разделы

Аффилиация

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