English
For a list xs of a commutative ordered monoid M, if x ∈ xs, then x ≤ xs.prod.
Русский
Пусть xs — список элементов M, тогда каждый элемент x списка не превосходит произведение xs.
LaTeX
$$$\\forall xs:\\, \\text{List } M,\\ \\forall x\\in xs,\\ x \\le xs.prod.$$
Lean4
/-- See also `List.le_prod_of_mem`. -/
@[to_additive /-- See also `List.le_sum_of_mem`. -/
]
theorem single_le_prod [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) :
∀ x ∈ l, x ≤ l.prod := by
induction l
· simp
simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
constructor
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)
