isPositive_toLinearMap_iff — Mathlib

English

Let T be a linear operator on the inner product space E that is continuous. Then T is positive as a linear map if and only if T is positive as a continuous linear map.

Русский

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

LaTeX

$$$ (T: E \to_{\mathbb{K}} E).IsPositive \ \\iff \ T.IsPositive $$$

Lean4

theorem isPositive_toLinearMap_iff (T : E →L[𝕜] E) : (T : E →ₗ[𝕜] E).IsPositive ↔ T.IsPositive := by
  simp only [LinearMap.IsPositive, ← isSelfAdjoint_iff_isSymmetric, coe_coe, IsPositive, reApplyInnerSelf]

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