prod_pos — Mathlib

English

If every element of a multiset s is positive, then the product is positive: 0 < s.prod.

Русский

Если каждый элемент мультиmножества положителен, то произведение положительно.

LaTeX

$$$$0 < \\prod_{a \\in s} a \\quad \\text{if } \\forall a \\in s, a > 0.$$$$

Lean4

theorem prod_pos {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_pos h

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