one_le_prod'' — Mathlib

English

Same as above: If every f(i) ≥ 1 for i in s, then 1 ≤ ∏_{i∈s} f(i).

Русский

То же самое: если для всех i ∈ s выполняется f(i) ≥ 1, то 1 ≤ ∏_{i∈s} f(i).

LaTeX

$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s : \\mathrm{Finset} \\iota}, [\\text{MulLeftMono } N], ( \\forall i \\in s, 1 \\le f(i) ) \\Rightarrow 1 \\le \\prod_{i \\in s} f(i). $$$

Lean4

@[to_additive Finset.sum_nonneg']
theorem one_le_prod'' [MulLeftMono N] (h : ∀ i : ι, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
  Finset.one_le_prod' fun i _ ↦ h i

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