Theorems · Theorem · order theory

Finset.prod_le_prod

∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f g : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

If all f i, i ∈ s, are nonnegative and each f i is less than or equal to g i, then the product of f i is less than or equal to the product of g i. See also Finset.prod_le_prod' for the case of an ordered commutative multiplicative monoid.

Defined in

Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Cited by

40 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroPreorderZeroLEOneClassPosMulMono