English
If each f(i) ≥ 0 and f(i) ≤ g(i) for all i in s, then the product of f over s is ≤ the product of g over s: (∏ f(i)) ≤ (∏ g(i)).
Русский
Если для всех i∈s выполняются f(i) ≥ 0 и f(i) ≤ g(i), то произведение f нечётко не превосходит произведение g: ∏ f(i) ≤ ∏ g(i).
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
theorem prod_map_le_prod_map₀ {ι : Type*} {s : List ι} (f : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 ≤ f i)
(h : ∀ i ∈ s, f i ≤ g i) : (map f s).prod ≤ (map g s).prod := by
induction s with
| nil => simp
| cons a s hind =>
simp only [map_cons, prod_cons]
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
apply mul_le_mul
· apply h
simp
· grind
· grind [prod_nonneg]
· apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]
