one_lt_prod — Mathlib

English

If every i in s has f(i) < 1, then the product over s is less than 1 (assuming s is nonempty).

Русский

Если для каждого i ∈ s выполнено f(i) < 1, то произведение по s меньше 1 (при непустом s).

LaTeX

$$$(\\forall i ∈ s, f(i) < 1) \\land s \\neq \\emptyset \\Rightarrow \\prod_{i ∈ s} f(i) < 1$$$

Lean4

@[to_additive sum_pos]
theorem one_lt_prod (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) : 1 < ∏ i ∈ s, f i :=
  lt_of_le_of_lt (by rw [prod_const_one]) <| prod_lt_prod_of_nonempty' hs h

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