list_prod_pos — Mathlib

English

A variant of product-positivity for lists: the list product is positive iff every element is positive.

Русский

Вариант положительности произведения для списков: произведение списка положительно тогда и только тогда, когда каждый элемент положителен.

LaTeX

$$$\text{0} < \text{List}.prod(l) \iff \forall x \in l, (0 < x)$$$

Lean4

/-- A variant of `List.prod_pos` for `CanonicallyOrderedAdd`. -/
@[simp]
theorem list_prod_pos {α : Type*} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α]
    [Nontrivial α] : ∀ {l : List α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
  | [] => by simp
  | (x :: xs) => by simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos, list_prod_pos]

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