inner_map_map_of_mem_unitary — Mathlib

English

If u is unitary, then the inner product is preserved: ⟪u x, u y⟫ = ⟪x, y⟫ for all x, y in H.

Русский

Если u — унитарный, то скалярное произведение сохраняется: ⟪u x, u y⟫ = ⟪x, y⟫ для любых x, y в H.

LaTeX

$$$\langle u x, u y\rangle = \langle x, y\rangle \quad\text{for all } x,y\in H$$$

Lean4

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

  have := unitary.star_mul_self_of_mem hu
  u.inner_map_map_iff_adjoint_comp_self.mpr this x y

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