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