English
Let M be a ordered monoid with monotone multiplication on both sides. Let l be a finite list of indices and f,g : ι → M. If f(i) ≤ g(i) for every i ∈ l and there exists i ∈ l with f(i) < g(i), then the product of f over l is strictly less than the product of g over l:
Русский
Пусть M — упорядоченная полунаборная (моноид) с монотонностью умножения слева и справа. Пусть l — конечный список индексов, и f,g : ι → M. Если для каждого i ∈ l выполняется f(i) ≤ g(i) и существует i ∈ l such that f(i) < g(i), то произведение f над l строго меньше произведения g над l:
LaTeX
$$$\\forall l:\\,\\text{List }\\iota,\\ \\forall f,g:\\iota\\to M,\\ [\\text{Preorder } M], [\\text{MulLeftStrictMono } M], [\\text{MulLeftMono } M], [\\text{MulRightStrictMono } M], [\\text{MulRightMono } M], \\\\ (\\forall i\\in l,\\ f(i) \\le g(i)) \\land (\\exists 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 sum_lt_sum]
theorem prod_lt_prod' [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M]
{l : List ι} (f g : ι → M) (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod :=
by
induction l with
| nil => simp at h₂
| cons i l ihl =>
simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
simp only [mem_cons, exists_eq_or_imp] at h₂
cases h₂
· exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
· exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›
