one_lt_prod' — Mathlib

English

If for all 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 \\in s, 1 \\le f(i) \\;\\land\\; \\exists i \\in s, 1 < f(i) \\Rightarrow 1 < \\prod_{i \\in s} f(i)$$$

Lean4

@[to_additive sum_pos']
theorem one_lt_prod' (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) : 1 < ∏ i ∈ s, f i :=
  prod_const_one.symm.trans_lt <| prod_lt_prod' h hs

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