Theorems · Theorem · order theory
Finset.sum_le_card_nsmul
∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] [AddLeftMono N] (s : Finset ι)
(f : ι → N) (n : N), (∀ x ∈ s, f x ≤ n) → s.sum f ≤ s.card • n- Cited by
- 25 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- LE.le.transproof · cited by 3,151
- Finset.cardstatement and proof · cited by 2,327
- Multiset.mapproof · cited by 876
- AddLeftMonostatement and proof · cited by 687
- Finset.valproof · cited by 438
- Multiset.mem_mapproof · cited by 72
- Multiset.card_mapproof · cited by 57
- Multiset.sum_le_card_nsmulproof · cited by 3
Cited by25
Results whose statement or proof uses this declaration.
- Finset.card_nsmul_le_sumproof · cited by 10
- MonovaryOn.sum_smul_sum_le_card_smul_sumproof · cited by 4
- MeasureTheory.uniformIntegrable_averageproof · cited by 2
- Finset.card_nsmul_le_card_nsmulproof · cited by 2
- Finset.card_biUnion_le_card_mulproof · cited by 2
- Finset.sum_card_inter_leproof · cited by 2
- AkraBazziRecurrence.eventually_atTop_sumTransform_leproof · cited by 1
- Finset.expect_leproof · cited by 1
- Finpartition.IsEquipartition.sum_nonUniforms_lt'proof · cited by 1
- MulAction.IsPreprimitive.of_card_ltproof · cited by 1
- Polynomial.natDegree_det_X_add_C_leproof · cited by 1
- bergelson'proof · cited by 1