isSelfAdjoint_iff_isSymmetric — Mathlib

English

For a bounded linear operator A on E, A is self-adjoint if and only if its underlying linear map is symmetric, i.e., ⟪Ax, y⟫ = ⟪x, Ay⟫ for all x,y ∈ E.

Русский

Для ограниченного линейного оператора A на E справедливо: A самосопряжённый тогда и только тогда, когда соответствующее линейное отображение симметрично, т.е. для всех x,y выполняется ⟪Ax, y⟫ = ⟪x, Ay⟫.

LaTeX

$$$\\text{IsSelfAdjoint}(A) \\iff (A : E \\to E) \\text{IsSymmetric}$$$

Lean4

theorem _root_.ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {A : E →L[𝕜] E} :
    IsSelfAdjoint A ↔ (A : E →ₗ[𝕜] E).IsSymmetric :=
  ⟨fun hA => hA.isSymmetric, fun hA =>
    ext fun x => ext_inner_right 𝕜 fun y => (A.adjoint_inner_left y x).symm ▸ (hA x y).symm⟩

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