Theorems · Definition · sequences and series
SummationFilter.symmetricIcc
(G : Type u_1) → [Neg G] → [inst : Preorder G] → [LocallyFiniteOrder G] → SummationFilter G
The SummationFilter on a locally finite order G corresponding to the symmetric
intervals Icc (-N) N·
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, 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.
- Preorderstatement and proof · cited by 7,952
- Filter.atTopproof · cited by 2,405
- Filter.mapproof · cited by 819
- LocallyFiniteOrderstatement and proof · cited by 658
- SummationFilterstatement · cited by 607
- Finset.Iccproof · cited by 348
Cited by17
Results whose statement or proof uses this declaration.
- EisensteinSeries.G2proof · cited by 10
- SummationFilter.symmetricIcc_eq_map_Icc_natstatement · cited by 3
- HasSum.hasSum_symmetricIco_of_hasSum_symmetricIccstatement and proof · cited by 3
- EisensteinSeries.hasSum_e2Summand_symmetricIccstatement · cited by 3
- SummationFilter.symmetricIcc_filterstatement and proof · cited by 2
- EisensteinSeries.summable_e2Summand_symmetricIccstatement · cited by 2
- HasProd.hasProd_symmetricIco_of_hasProd_symmetricIccstatement and proof · cited by 2
- SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIcostatement and proof · cited by 1
- EisensteinSeries.G2_eq_tsum_symmetricIcoproof · cited by 1
- Summable.tendsto_zero_of_even_summable_symmetricIccstatement and proof · cited by 1
- SummationFilter.symmetricIcc_eq_symmetricIoo_intstatement · cited by 0
- SummationFilter.symmetricIcc_le_Conditionalstatement · cited by 0