add — Mathlib

English

If A and B are positive definite, then A+B is positive definite.

Русский

Если A и B положительно определены, то A+B положительно определено.

LaTeX

$$$$ \\operatorname{PosDef}(A) \\to \\operatorname{PosDef}(B) \\to \\operatorname{PosDef}(A+B). $$$$

Lean4

protected theorem add [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosDef) (hB : B.PosDef) :
    (A + B).PosDef :=
  hA.add_posSemidef hB.posSemidef

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