max_prod_le — Mathlib

English

If every element of a list l of a commutative ordered monoid M is at least 1, then the product l.prod is at least 1.

Русский

Если каждый элемент списка l в коммутативном упорядоченном моноиде M не меньше 1, то произведение l.prod не меньше 1.

LaTeX

$$$\\forall l:\\, \\text{List } M,\\ (\\forall x\\in l,\\ 1 \\le x) \\Rightarrow 1 \\le l.prod.$$

Lean4

@[to_additive]
theorem max_prod_le (l : List α) (f g : α → M) [LinearOrder M] [MulLeftMono M] [MulRightMono M] :
    max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod :=
  by
  rw [max_le_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply le_max_left
  · apply le_max_right

Похожие утверждения