English
In the same ordered setting, the product of pairwise minima is bounded above by the minimum of the two products: ∏_{i∈s} min(f(i), g(i)) ≤ min(∏_{i∈s} f(i), ∏_{i∈s} g(i)).
Русский
В той же упорядоченной структуре произведение попарных минимумов не превосходит минимум из двух произведений: ∏ min(f(i), g(i)) ≤ min(∏ f(i), ∏ g(i)).
LaTeX
$$$$\\prod_{i \\in s} \\min\\bigl(f(i), g(i)\\bigr) \\le \\min\\Bigl(\\prod_{i \\in s} f(i), \\prod_{i \\in s} g(i)\\Bigr).$$$$
Lean4
@[to_additive]
theorem prod_min_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} :
(s.map fun i ↦ min (f i) (g i)).prod ≤ min (s.map f).prod (s.map g).prod :=
by
obtain ⟨l⟩ := s
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
apply List.prod_min_le
