prod_pos — Mathlib

English

If a function f has all values positive on a finite set s, then the product over s is positive; conversely, if the product is positive, each factor is positive when none are zero divisors.

Русский

Если все значения функции f на конечном множестве s положительны, то произведение по s положительно; обратно, если произведение положительно, то каждый фактор положителен (при условии отсутствия нулевых делителей).

LaTeX

$$0 < ∏_{i∈s} f(i) ↔ ∀ i∈s, 0 < f(i)$$

Lean4

/-- Note that the name is to match `CanonicallyOrderedAdd.mul_pos`. -/
@[simp]
theorem _root_.CanonicallyOrderedAdd.prod_pos [NoZeroDivisors R] [Nontrivial R] :
    0 < ∏ i ∈ s, f i ↔ (∀ i ∈ s, (0 : R) < f i) :=
  CanonicallyOrderedAdd.multiset_prod_pos.trans Multiset.forall_mem_map_iff

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