smul — Mathlib

English

If B is a nonnegative sesquilinear form and c is a nonnegative scalar, then the scaled form c·B is again nonnegative.

Русский

Если B — неотрицательная полусферическая (сесквилинейная) форма и c ≥ 0, то масштабированная форма c·B также неотрицательна.

LaTeX

$$$\big(\forall x,\ B(x,x) \ge 0\big) \land (0 \le c) \Rightarrow \forall x,\ (c\cdot B)(x,x) \ge 0$$$

Lean4

protected theorem smul [Preorder R] [PosMulMono R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R} {c : R} (hB : B.IsNonneg) (hc : 0 ≤ c) :
    (c • B).IsNonneg where nonneg x := mul_nonneg hc (hB.nonneg x)

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