prod_nonneg — Mathlib

English

For a list of nonnegative elements, the product is nonnegative: if every a ∈ s satisfies 0 ≤ a, then the product s.prod ≥ 0.

Русский

Если все элементы списка неотрицательны, то их произведение неотрицательно: при любом списке s, если для каждого a ∈ s верно 0 ≤ a, то s.prod ≥ 0.

LaTeX

$$$$0 \\le \\prod_{i \\in s} a_i \\quad \\text{whenever} \\quad a_i \\ge 0 \\text{ for all } i \\in s.$$$$

Lean4

theorem prod_nonneg {s : List R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod := by
  induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)

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