finprod_cond_nonneg — Mathlib

English

If R is ordered and f ≥ 0 pointwise, then the finprod is nonnegative: ∏ᶠ (x) p x, f x ≥ 0.

Русский

Если R упорядочено и f(x) ≥ 0 для всех x, то финпроизведение неотрицательно.

LaTeX

$$$0 \\le \\prod^\\!x, p x, f x$$$

Lean4

theorem finprod_cond_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {p : α → Prop} {f : α → R}
    (hf : ∀ x, p x → 0 ≤ f x) : 0 ≤ ∏ᶠ (x) (_ : p x), f x :=
  finprod_nonneg fun x => finprod_nonneg <| hf x

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