prod_pos

Mathlib.Algebra.Order.BigOperators.Ring.Finset

URI: https://scilib.ai/kg/mathlib#Finset.prod_pos

English

(Duplicate) If all f(i) > 0 for i in s, then the product is positive.

Русский

(Дублировано) Если все f(i) > 0 для i в s, то произведение положительно.

LaTeX

$$$$0 < \\prod_{i ∈ s} f(i) \\quad \\text{если } \\forall i ∈ s, f(i) > 0.$$$$

Lean4

theorem prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i :=
  prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru