English
For any f,g : ι → M in a commutative monoid M with a linear order, the maximum of the two products is bounded by the product of pointwise maxima: max(∏ f, ∏ g) ≤ ∏ max(f(i), g(i)).
Русский
Для любых f,g : ι → M в упорядоченном коммутативном моноиде M выполняется: max(∏ f, ∏ g) ≤ ∏ max(f(i), g(i)).
LaTeX
$$$ \\forall s : \\mathrm{Finset} \\iota, f,g : \\iota \\to M\\, [\\text{CommMonoid } M], [\\text{LinearOrder } M], [\\text{IsOrderedMonoid } M], \\max\\left( \\prod_{i\\in s} f(i), \\prod_{i\\in s} g(i) \\right) \\le \\prod_{i\\in s} \\max\\bigl( f(i), g(i) \\bigr). $$$
Lean4
@[to_additive]
theorem max_prod_le [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
max (s.prod f) (s.prod g) ≤ s.prod (fun i ↦ max (f i) (g i)) :=
Multiset.max_prod_le
