Theorems · Theorem · group theory

finprod_le_finprod

∀ {α : Type u_1} {M : Type u_7} [inst : CommMonoidWithZero M] [inst_1 : PartialOrder M] [ZeroLEOneClass M]
  [PosMulMono M] {f g : α → M},
  Function.HasFiniteMulSupport f →
    (∀ (a : α), 0 ≤ f a) → Function.HasFiniteMulSupport g → f ≤ g → ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Monotonicity of finprod. See finprod_le_finprod' for a variant where M is an ordered CommMonoid.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroPartialOrderZeroLEOneClassPosMulMono