Theorems · Inductive type · sequences and series
SummationFilter
Type u_4 → Type u_4
A filter on the set of finite subsets of a type β. (Used for defining infinite topological
sums and products, as limits along the given filter of partial sums / products over finsets.)
- Cited by
- 607 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by648
Results whose statement or proof uses this declaration.
- SummationFilter.unconditionalstatement · cited by 2,068
- tsumstatement · cited by 1,148
- Summablestatement and proof · cited by 778
- HasSumstatement and proof · cited by 518
- tprodstatement · cited by 230
- Multipliablestatement and proof · cited by 213
- Summable.hasSumstatement and proof · cited by 184
- HasProdstatement and proof · cited by 157
- HasSum.tsum_eqstatement and proof · cited by 150
- SummationFilter.NeBotstatement · cited by 130
- SummationFilter.filterstatement and proof · cited by 110
- HasSum.summablestatement and proof · cited by 98
Showing the 200 most cited of 648.