Theorems · Theorem · general topology
NNReal.summable_coe
∀ {α : Type u_2} {L : SummationFilter α} {f : α → NNReal}, Summable (fun a => ↑(f a)) L ↔ Summable f L- Defined in
- Mathlib.Topology.Instances.NNReal.Lemmas
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finsetproof · cited by 13,712
- nhdsproof · cited by 5,554
- Finset.sumproof · cited by 5,195
- Bot.botproof · cited by 4,720
- NNRealstatement and proof · cited by 4,310
- Filter.Tendstoproof · cited by 3,814
- Finset.sum_congrproof · cited by 2,323
- NNReal.toRealstatement and proof · cited by 1,260
- Summablestatement and proof · cited by 778
- SummationFilterstatement and proof · cited by 607
- HasSumproof · cited by 518
Cited by15
Results whose statement or proof uses this declaration.
- Summable.of_nonneg_of_leproof · cited by 36
- Summable.of_nnnorm_boundedproof · cited by 4
- NNReal.summable_comp_injectiveproof · cited by 3
- MeasureTheory.setToFun_tsumproof · cited by 3
- ENNReal.tsum_coe_ne_top_iff_summable_coeproof · cited by 2
- NNReal.summable_nat_add_iffproof · cited by 2
- MeasureTheory.hasSum_integral_of_summable_integral_normproof · cited by 2
- HasFPowerSeriesWithinAt.compproof · cited by 2
- Summable.toNNRealproof · cited by 1
- Summable.countable_support_nnrealproof · cited by 1
- MeasureTheory.integrableOn_iUnion_of_summable_integral_normproof · cited by 1
- FormalMultilinearSeries.summable_nnnorm_mul_powproof · cited by 1