English
For a finite list l and maps f,g: α → M, the maximum of the two products is bounded by the product of pairwise maxima: max(∏ f, ∏ g) ≤ ∏ max(f(i), g(i)).
Русский
Для конечного списка l и отображений f,g: α → M максимум двух произведений не больше произведения попарно максимумов: max(∏ f, ∏ g) ≤ ∏ max(f(i), g(i)).
LaTeX
$$$\\max\\left((l.map f).prod,\\ (l.map g).prod\\right) \\le (l.map (\\lambda i.\\max (f i) (g i))).prod.$$
Lean4
@[to_additive sum_nonneg]
theorem one_le_prod_of_one_le [Preorder M] [MulLeftMono M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : 1 ≤ l.prod := by
-- We don't use `pow_card_le_prod` to avoid assumption
-- [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)]
induction l with
| nil => rfl
| cons hd tl ih =>
rw [prod_cons]
exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))
