norm_map' — Mathlib

English

If a map f is an isometry between normed groups and sends 1 to 1, then ‖f x‖ = ‖x‖ for all x.

Русский

Если отображение f является изометрией между нормированными группами и отправляет 1 в 1, то ‖f x‖ = ‖x‖ для всех x.

LaTeX

$$$\\text{If } f\\text{ is an isometry and } f(1)=1, \\text{ then } \\|f(x)\\| = \\|x\\|\\text{ for all } x$$$

Lean4

@[to_additive (attr := simp) norm_map]
theorem norm_map' [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖ = ‖x‖ :=
  (IsometryClass.isometry f).norm_map_of_map_one (map_one f) x

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