English
For a finite list l and maps f,g: α → M with M linearly ordered, the product of pairwise minima is at most the minimum of the two products: ∏ min(f(i), g(i)) ≤ min(∏ f(i), ∏ g(i)).
Русский
Для конечного списка l и отображений f,g: α → M в линейно упорядкованном M произведение попарных минимумов не превосходит минимум из двух произведений: ∏ min(f(i), g(i)) ≤ min(∏ f(i), ∏ g(i)).
LaTeX
$$$\\forall l:\\,\\text{List } \\alpha,\\ f,g:\\alpha\\to M,\\ (\\prod_{i\\in l} \\min(f(i),g(i))) \\le \\min\\left(\\prod_{i\\in l} f(i),\\prod_{i\\in l} g(i)\\right).$$
Lean4
@[to_additive]
theorem prod_min_le [LinearOrder M] [MulLeftMono M] [MulRightMono M] (l : List α) (f g : α → M) :
(l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod :=
by
rw [le_min_iff]
constructor <;> apply List.prod_le_prod' <;> intros
· apply min_le_left
· apply min_le_right
