add — Mathlib

English

If B and C are positive semidefinite, then their sum B+C is positive semidefinite.

Русский

Если B и C положительно полусобственны, то их сумма B+C тоже положительно полусобственна.

LaTeX

$$$(\text{IsPosSemidef}(B) \land \text{IsPosSemidef}(C)) \Rightarrow \text{IsPosSemidef}(B+C)$$$

Lean4

protected theorem add [Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₗ[R] R} (hB : B.IsPosSemidef)
    (hC : C.IsPosSemidef) : (B + C).IsPosSemidef :=
  isPosSemidef_def.2 ⟨hB.isSymm.add hC.isSymm, hB.isNonneg.add hC.isNonneg⟩

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