prod_le_univ_prod_of_one_le' — Mathlib

English

If every f(x) ≥ 1 for x ∈ ι, then the product over any finite subset s is ≤ the product over the entire ι.

Русский

Если для всех x ∈ ι верно f(x) ≥ 1, то произведение по любому конечному подмножеству s не превосходит произведение по всему ι.

LaTeX

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

Lean4

@[to_additive sum_le_univ_sum_of_nonneg]
theorem prod_le_univ_prod_of_one_le' [MulLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) :
    ∏ x ∈ s, f x ≤ ∏ x, f x :=
  prod_le_prod_of_subset_of_one_le' (subset_univ s) fun a _ _ ↦ w a

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