prod_mono_set_of_one_le' — Mathlib

English

If a family of positive factors is defined by a nonnegative function, the product is monotone in the set argument: enlarging the index set increases the product.

Русский

Если набор индексов расширяется, произведение не уменьшается при фиксации неотрицательных коэффициентов.

LaTeX

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

Lean4

@[to_additive sum_mono_set_of_nonneg]
theorem prod_mono_set_of_one_le' [MulLeftMono N] (hf : ∀ x, 1 ≤ f x) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hst ↦
  prod_le_prod_of_subset_of_one_le' hst fun x _ _ ↦ hf x

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