Theorems · Definition · sequences and series
SummationFilter.conditional
(β : Type u_2) → [inst : Preorder β] → [LocallyFiniteOrder β] → SummationFilter β
Conditional summation, for ordered types β such that closed intervals [x, y] are
finite: this corresponds to limits of finite sums over larger and larger intervals.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PreorderLocallyFiniteOrder
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.
- Preorderstatement and proof · cited by 7,952
- Filter.atTopproof · cited by 2,405
- SProd.sprodproof · cited by 1,750
- Filter.mapproof · cited by 819
- LocallyFiniteOrderstatement and proof · cited by 658
- SummationFilterstatement · cited by 607
- Filter.atBotproof · cited by 512
- Finset.Iccproof · cited by 348
Cited by14
Results whose statement or proof uses this declaration.
- SchauderBasisproof · cited by 12
- SummationFilter.conditional_filterstatement and proof · cited by 2
- SchauderBasis.proj_applystatement · cited by 1
- SummationFilter.conditional_filter_eq_map_Iicstatement · cited by 1
- SummationFilter.conditional_filter_eq_map_rangestatement · cited by 1
- SchauderBasis.tendsto_projproof · cited by 1
- SummationFilter.symmetricIcc_le_Conditionalstatement · cited by 0
- SchauderBasis.proj_apply_basis_memstatement · cited by 0
- SchauderBasis.proj_compproof · cited by 0
- SchauderBasis.range_proj_eq_spanstatement · cited by 0
- SchauderBasis.RankOneDecomposition.basis_coestatement · cited by 0
- SummationFilter.conditional_filter_eq_map_Icistatement · cited by 0