add — Mathlib

English

If T is positive, then for any S, the composed operator S ∘ T ∘ S† is positive.

Русский

Если T положителен, то для любого S оператор S ∘ T ∘ S† положителен.

LaTeX

$$$\text{IsPositive}(S \circ_L T \circ_L S^\dagger) \,\text{ holds for any } S$$$

Lean4

@[aesop safe apply]
theorem add {T S : E →L[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) : (T + S).IsPositive :=
  (isPositive_toLinearMap_iff _).mp (hT.toLinearMap.add hS.toLinearMap)

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