edist_map

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

Diameter is preserved under the image of a set by a linear isometry.

Русский

Диаметр множества сохраняется при взятии образа линейной изометрией.

LaTeX

$$EDiam(f''S) = EDiam(S)$$

Lean4

@[simp]
theorem edist_map (x y : E) : edist (f x) (f y) = edist x y :=
  f.isometry.edist_eq x y

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

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

Разделы

Аффилиация

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