one_le_prod — Mathlib

English

If every element of a list is at least 1, then the product is at least 1: 1 ≤ ∏ a_i when ∀ i, a_i ≥ 1.

Русский

Если каждый элемент списка не меньше единицы, то произведение не меньше единицы: 1 ≤ ∏ a_i.

LaTeX

$$$$1 \\le \\prod_{i \\in s} a_i \\quad \\text{whenever} \\quad a_i \\ge 1 \\text{ for all } i \\in s.$$$$

Lean4

theorem one_le_prod {s : List R} (h : ∀ a ∈ s, 1 ≤ a) : 1 ≤ s.prod := by
  induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

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