le_prod_of_mem — Mathlib

English

In a canonically ordered monoid, every element of a list is less than or equal to the product of the list.

Русский

В канонически упорядоченном моноиде каждый элемент списка не превосходит произведение списка.

LaTeX

$$$\\forall xs:\\, \\text{List } M,\\ x\\in xs \\Rightarrow x \\le xs.prod.$$

Lean4

/-- See also `List.single_le_prod`. -/
@[to_additive /-- See also `List.single_le_sum`. -/
    ]
theorem le_prod_of_mem {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod := by
  induction xs with
  | nil => simp at h₁
  | cons y ys ih =>
    simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

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