norm_map — Mathlib

English

For a unitary element u in the unitary group, the induced linear map has norm-preserving property: ∥u x∥ = ∥x∥ for all x.

Русский

Для элемента u из унитарной группы отображение сохраняет норму: ∥u x∥ = ∥x∥ для всех x.

LaTeX

$$$\|u x\| = \|x\|\quad\text{for all } x$$$

Lean4

theorem norm_map (u : unitary (H →L[𝕜] H)) (x : H) : ‖(u : H →L[𝕜] H) x‖ = ‖x‖ :=
  u.val.norm_map_of_mem_unitary u.property x

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