posSemidef_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem posSemidef_add [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosSemidef)
    (hB : B.PosDef) : (A + B).PosDef :=
  add_comm A B ▸ hB.add_posSemidef hA

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