norm_eq_of_isometry

Mathlib.Analysis.Normed.Group.Hom

URI: https://scilib.ai/kg/mathlib#NormedAddGroupHom.norm_eq_of_isometry

English

If f is an isometry, then for all v, ∥f(v)∥ = ∥v∥.

Русский

Если f изометрия, то для любого v выполнено ∥f(v)∥ = ∥v∥.

LaTeX

$$$\\|f(v)\\| = \\|v\\|$$$

Lean4

theorem norm_eq_of_isometry {f : NormedAddGroupHom V W} (hf : Isometry f) (v : V) : ‖f v‖ = ‖v‖ :=
  (AddMonoidHomClass.isometry_iff_norm f).mp hf v

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

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

Разделы

Аффилиация

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