English
If a finite list s is nonempty, a_i < b_i for each i and a_i > 0, then the product of a_i is strictly less than the product of b_i: ∏ a_i < ∏ b_i.
Русский
Если непустой набор индексов u имеет элемент a_i меньше b_i и все a_i > 0, то произведение a_i меньше произведения b_i: ∏ a_i < ∏ b_i.
LaTeX
$$$$\\left(\\prod_{i \\in s} a_i\\right) < \\left(\\prod_{i \\in s} b_i\\right) \\quad \\text{if } 0 < a_i \\text{ and } a_i < b_i \\text{ for all } i \\in s.$$$$
Lean4
theorem prod_map_lt_prod_map {ι : Type*} {s : List ι} (hs : s ≠ []) (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
match s with
| [] => contradiction
| a :: s =>
simp only [map_cons, prod_cons]
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
apply mul_lt_mul
· apply h
simp
· apply prod_map_le_prod_map₀
· intro i hi
apply le_of_lt
apply h0
simp [hi]
· intro i hi
apply le_of_lt
apply h
simp [hi]
· apply prod_pos
grind
· apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp
