isSelfAdjoint_toLinearMap_iff — Mathlib

English

A continuous linear map T is self-adjoint iff its corresponding linear map is self-adjoint.

Русский

Пусть непрерывное линейное отображение T самосопряжённо тогда и только тогда, когда соответствующее линейное отображение тоже самосопряжено.

LaTeX

$$$$\text{IsSelfAdjoint}(T) \iff \text{IsSelfAdjoint}(T^{\text{toLinearMap}}).$$$$

Lean4

theorem _root_.ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff (T : E →L[𝕜] E) :
    have := FiniteDimensional.complete 𝕜 E
    IsSelfAdjoint T.toLinearMap ↔ IsSelfAdjoint T :=
  by
  simp only [IsSelfAdjoint, star, adjoint, LinearEquiv.trans_apply, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]
  rfl

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