Theorems · Theorem · order theory
Finset.single_le_sum
∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
[AddLeftMono N], (∀ i ∈ s, 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x ∈ s, f x- Cited by
- 34 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- AddLeftMonostatement and proof · cited by 687
- Finset.sum_singletonproof · cited by 251
- Finset.singleton_subset_iffproof · cited by 38
- Finset.sum_le_sum_of_subset_of_nonnegproof · cited by 31
Cited by34
Results whose statement or proof uses this declaration.
- Function.hasTemperateGrowth_one_add_norm_sq_rpowproof · cited by 9
- summable_norm_iffproof · cited by 8
- mem_Icc_of_mem_stdSimplexproof · cited by 3
- Finset.single_le_sum_of_canonicallyOrderedproof · cited by 2
- Real.posLog_sumproof · cited by 2
- ArithmeticFunction.vonMangoldt_le_logproof · cited by 2
- Finset.geomSum_ofColex_strictMonoproof · cited by 2
- WithCStarModule.norm_apply_le_normproof · cited by 2
- FormalMultilinearSeries.le_radius_piproof · cited by 2
- MvPolynomial.degreeOf_le_totalDegreeproof · cited by 1
- single_le_finsumproof · cited by 1