Theorems · Definition · sequences and series
SummationFilter.support
{β : Type u_2} → SummationFilter β → Set βThe support of a summation filter (its lim inf, considered as a filter of sets).
- Cited by
- 36 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Finsetproof · cited by 13,712
- Set.ofPredproof · cited by 6,101
- Filter.Eventuallyproof · cited by 3,134
- SummationFilterstatement and proof · cited by 607
- SummationFilter.filterproof · cited by 110
Cited by38
Results whose statement or proof uses this declaration.
- Summable.hasSumproof · cited by 184
- Multipliable.hasProdproof · cited by 88
- tsum_zeroproof · cited by 63
- tprod_oneproof · cited by 12
- tsum_defstatement and proof · cited by 11
- tprod_defstatement and proof · cited by 11
- SummationFilter.support_eq_univstatement · cited by 10
- tprod_botproof · cited by 6
- tsum_botproof · cited by 6
- SummationFilter.HasSupport.eventually_le_supportstatement · cited by 5
- tsum_eq_finsumproof · cited by 4
- summable_of_ne_finset_zeroproof · cited by 4