Theorems · Theorem · order theory

Finset.le_prod_of_submultiplicative_on_pred_of_nonneg

∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {M : Type u_4}
  [inst_3 : CommMonoid M] (f : M → R) (p : M → Prop),
  (∀ (a : M), 0 ≤ f a) →
    f 1 ≤ 1 →
      (∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b) →
        (∀ (a b : M), p a → p b → p (a * b)) →
          ∀ (s : Finset ι) (g : ι → M), (∀ a ∈ s, p (g a)) → f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Defined in

Mathlib.Algebra.Order.BigOperators.Ring.Finset

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringPartialOrderIsOrderedRingCommMonoid