English
If l is a nonempty list of indices and f,g : ι → M satisfy f(i) < g(i) for every i ∈ l, then the product of f over l is strictly less than the product of g over l.
Русский
Пусть l — непустой список индексов и f,g : ι → M удовлетворяют f(i) < g(i) для каждого i ∈ l; тогда произведение f над l строго меньше произведения g над l.
LaTeX
$$$\\forall l:\\, \\text{List }\\iota,\\ f,g:\\iota\\to M,\\ (\\forall i\\in l,\\ f(i) < g(i)) \\Rightarrow \\left(\\prod_{i\\in l} f(i)\\right) < \\left(\\prod_{i\\in l} g(i)\\right).$$
Lean4
@[to_additive]
theorem prod_lt_prod_of_ne_nil [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M]
[MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (hlt : ∀ i ∈ l, f i < g i) :
(l.map f).prod < (l.map g).prod :=
(prod_lt_prod' f g fun i hi => (hlt i hi).le) <| (exists_mem_of_ne_nil l hl).imp fun i hi => ⟨hi, hlt i hi⟩
