prod_nonneg — Mathlib

English

If every f(i) ≥ 0 for i in s, then the finite product ∏ f(i) is nonnegative.

Русский

Если для всех i в s f(i) ≥ 0, то конечное произведение неотрицательно.

LaTeX

$$$$0 \\le \\prod_{i ∈ s} f(i) \\quad \\text{given } \\forall i ∈ s, f(i) \\ge 0.$$$$

Lean4

theorem prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i :=
  prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0

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