Theorems · Theorem · order theory
Finset.card_nsmul_le_sum
∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] [AddLeftMono N] (s : Finset ι)
(f : ι → N) (n : N), (∀ x ∈ s, n ≤ f x) → s.card • n ≤ s.sum f- Cited by
- 10 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Preorderstatement and proof · cited by 7,952
- Finset.sumstatement · cited by 5,195
- Finset.cardstatement · cited by 2,327
- AddLeftMonostatement and proof · cited by 687
- Finset.sum_le_card_nsmulproof · cited by 25
Cited by10
Results whose statement or proof uses this declaration.
- Finset.card_nsmul_le_card_nsmulproof · cited by 2
- MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotentproof · cited by 2
- Finset.le_sum_card_interproof · cited by 2
- AkraBazziRecurrence.eventually_atTop_sumTransform_geproof · cited by 1
- SimpleGraph.triangle_counting'proof · cited by 1
- Finset.le_expectproof · cited by 1
- Finset.card_nsmul_lt_card_nsmul_of_le_of_ltproof · cited by 1
- bergelson'proof · cited by 1
- Finset.sum_Ico_le_sumproof · cited by 1
- Finset.sum_le_sum_Iocproof · cited by 1