prod_lt_one — Mathlib

English

If for every i ∈ s we have 1 ≤ f(i) and there exists i ∈ s with 1 < f(i), then 1 < ∏_{i∈s} f(i).

Русский

Если для каждого i ∈ s верно 1 ≤ f(i) и существует i ∈ s с 1 < f(i), тогда 1 < ∏_{i∈s} f(i).

LaTeX

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

Lean4

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

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