add — Mathlib

English

The sum of two nonnegative sesquilinear maps is nonnegative.

Русский

Сумма двух неотрицательных сескаллинейных карт неотрицательна.

LaTeX

$$[Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₛₗ[I₂] R} (B.IsNonneg) (C.IsNonneg) → (B+C).IsNonneg$$

Lean4

protected theorem add [Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₛₗ[I₂] R} (hB : B.IsNonneg) (hC : C.IsNonneg) :
    (B + C).IsNonneg where nonneg x := add_nonneg (hB.nonneg x) (hC.nonneg x)

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