one_lt_prod_iff — Mathlib

English

For Finset s, the product of f over s is less than the product over g if each f(i) ≤ g(i) and there exists i with strict inequality.

Русский

Для конечного множества s произведение f по s меньше произведения g по s если f(i) ≤ g(i) для всех i и существует i с строгим неравенством.

LaTeX

$$$\\forall i ∈ s,\n f(i) ≤ g(i) \\quad\\text{and}\\quad \\exists i ∈ s, f(i) < g(i) \\Rightarrow \\prod_{i ∈ s} f(i) ≤ \\prod_{i ∈ s} g(i)$$

Lean4

@[to_additive sum_pos_iff]
theorem one_lt_prod_iff : 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x :=
  have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  Finset.one_lt_prod_iff_of_one_le <| fun _ _ => one_le _

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