inner_map_map — Mathlib

English

For a unitary u, the inner product satisfies ⟪u x, u y⟫ = ⟪x, y⟫ for all x,y.

Русский

Для унитарного уравнения выполняется ⟪u x, u y⟫ = ⟪x, y⟫ для любых x,y.

LaTeX

$$$\langle u x, u y\rangle = \langle x, y\rangle$ for all x,y$$

Lean4

theorem inner_map_map (u : unitary (H →L[𝕜] H)) (x y : H) : ⟪(u : H →L[𝕜] H) x, (u : H →L[𝕜] H) y⟫_𝕜 = ⟪x, y⟫_𝕜 :=
  u.val.inner_map_map_of_mem_unitary u.property x y

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