Theorems · Theorem · order theory

Finset.prod_lt_prod_of_subset_erase_union_singleton

∀ {ι : Type u_9} {M : Type u_10} [inst : DecidableEq ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [CanonicallyOrderedMul M] [MulLeftStrictMono M] {S S' : Finset ι} {f : ι → M} {d d' : ι},
  d ∈ S → S' ⊆ S.erase d ∪ {d'} → f d' < f d → ∏ x ∈ S', f x < ∏ x ∈ S, f x

In a canonically-ordered monoid, if S' is contained in (S.erase d) ∪ {d'} and f d' < f d for some d ∈ S, then the product of f over S' is strictly less than over S.

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqCommMonoidPartialOrderCanonicallyOrderedMulMulLeftStrictMono