finprod_nonneg — Mathlib

English

If every f x is nonnegative in a totally ordered commutative semiring, then the finprod is nonnegative.

Русский

Если каждый f x неотрицателен в упорядоченном коммутативном полугруппе, то финпроизводство неотрицательно.

LaTeX

$$$\\forall x, 0 \\le f(x) \\Rightarrow 0 \\le \\mathrm{finprod}(f)$$$

Lean4

theorem finprod_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f : α → R} (hf : ∀ x, 0 ≤ f x) :
    0 ≤ ∏ᶠ x, f x :=
  finprod_induction (fun x => 0 ≤ x) zero_le_one (fun _ _ => mul_nonneg) hf

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