prod_nonneg — Mathlib

English

The same nonnegativity of products extends to multisets: if every element of a multiset s is nonnegative, then s.prod ≥ 0.

Русский

Неотрицательность произведения переносится на мультимножество: если каждый элемент с неотрицателен, то произведение неотрицательно.

LaTeX

$$$$0 \\le \\text{Multiset}.prod(s) \\quad \\text{given } \\forall a \\in s, 0 \\le a.$$$$

Lean4

theorem prod_nonneg {s : Multiset R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod :=
  by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
  apply List.prod_nonneg h

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