English
If all f(i) ≥ 0 and f(i) ≤ g(i) for i ∈ s, then ∏ f(i) ≤ ∏ g(i).
Русский
Если для всех i∈s выполняются f(i) ≥ 0 и f(i) ≤ g(i), то произведение f(i) по s не превосходит произведение g(i) по s.
LaTeX
$$$$\\prod_{i \\in s} f(i) \\le \\prod_{i \\in s} g(i) \\quad \\text{given } f(i) \\ge 0\\text{ and } f(i) \\le g(i) .$$$$
Lean4
/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
the case of an ordered commutative multiplicative monoid. -/
@[gcongr]
theorem prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s has ih =>
simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
gcongr
exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
