norm_map_of_mem_unitary — Mathlib

English

If u is a unitary endomorphism of H, then it preserves norms: ∥u x∥ = ∥x∥ for all x ∈ H.

Русский

Если u — унитарный эндоморфизм пространства H, то он сохраняет норму: для всех x ∈ H выполняется ∥u x∥ = ∥x∥.

LaTeX

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

Lean4

theorem norm_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H) : ‖u x‖ = ‖x‖ :=
  -- Elaborates faster with this broken out https://github.com/leanprover-community/mathlib4/issues/11299

  have := unitary.star_mul_self_of_mem hu
  u.norm_map_iff_adjoint_comp_self.mpr this x

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