one_le_prod_of_one_le — Mathlib

English

If every element x of a multiset s satisfies 1 ≤ x in a ordered monoid, then 1 ≤ s.prod.

Русский

Если для каждой x ∈ s выполняется 1 ≤ x в упорядоченном моноиде, то 1 ≤ s.prod.

LaTeX

$$$ (\forall x \in s, 1 \le x) \implies 1 \le s.prod $$$

Lean4

@[to_additive sum_nonneg]
theorem one_le_prod_of_one_le [MulLeftMono α] : (∀ x ∈ s, (1 : α) ≤ x) → 1 ≤ s.prod :=
  Quotient.inductionOn s fun l hl => by simpa using List.one_le_prod_of_one_le hl

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