one_le_prod — Mathlib

English

If every element of a multiset s is at least 1, then the product is at least 1: 1 ≤ s.prod.

Русский

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

LaTeX

$$$$1 \\le \\prod_{a \\in s} a \\quad \\text{whenever } a \\ge 1 \\text{ for all } a \\in s.$$$$

Lean4

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

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