add — Mathlib

English

If T and S are positive endomorphisms, then T + S is positive.

Русский

Если T и S — положительные эндоморфизмы, то T + S положителен.

LaTeX

$$$$\text{If } T, S \text{ are positive, then } T + S \text{ is positive}.$$$$

Lean4

@[aesop safe apply]
theorem add {T S : E →ₗ[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) : (T + S).IsPositive :=
  by
  refine ⟨hT.isSymmetric.add hS.isSymmetric, fun x => ?_⟩
  rw [add_apply, inner_add_left, map_add]
  exact add_nonneg (hT.re_inner_nonneg_left x) (hS.re_inner_nonneg_left x)

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