prod_pos — Mathlib

English

If every element of a list is positive, then their product is positive: 0 < ∏ a_i when ∀ i, a_i > 0.

Русский

Если каждый элемент списка положителен, то их произведение положительно: 0 < ∏ a_i.

LaTeX

$$$$0 < \\prod_{i \\in s} a_i \\quad \\text{if } a_i > 0 \\text{ for all } i \\in s.$$$$

Lean4

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

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