prod_lt_prod_of_nonempty' — Mathlib

English

If s is nonempty and for every i ∈ s we have f(i) < g(i), then ∏_{i∈s} f(i) < ∏_{i∈s} g(i).

Русский

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

LaTeX

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

Lean4

/-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
strictly less than the corresponding factor `g i` of another nontrivial finite product, then
`s.prod f < s.prod g`. -/
@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) : ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
  Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt

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