isSelfAdjoint_toContinuousLinearMap_iff

English

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

Русский

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

LaTeX

$$$$\text{IsSelfAdjoint}(A) \iff \text{IsSelfAdjoint}(A^{\text{toContinuousLinearMap}}).$$$$

Lean4

theorem isSelfAdjoint_toContinuousLinearMap_iff (T : E →ₗ[𝕜] E) :
    have := FiniteDimensional.complete 𝕜 E
    IsSelfAdjoint T.toContinuousLinearMap ↔ IsSelfAdjoint T :=
  by simp [IsSelfAdjoint, star, adjoint, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]

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