Theorems · Definition · sequences and series
SummationFilter.symmetricIco
(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 Ico (-N) N·
- Cited by
- 17 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.Icoproof · cited by 450
Cited by17
Results whose statement or proof uses this declaration.
- HasSum.hasSum_symmetricIco_of_hasSum_symmetricIccstatement · cited by 3
- HasProd.hasProd_symmetricIco_of_hasProd_symmetricIccstatement · cited by 2
- EisensteinSeries.hasSum_e2Summand_symmetricIcostatement · cited by 1
- SummationFilter.symmetricIco_filterstatement and proof · cited by 1
- SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIcostatement · cited by 1
- EisensteinSeries.G2_eq_tsum_symmetricIcostatement and proof · cited by 1
- SummationFilter.hasSum_symmetricIco_int_iffstatement · cited by 1
- EisensteinSeries.summable_e2Summand_symmetricIcostatement · cited by 1
- EisensteinSeries.tendsto_double_sum_S_actproof · cited by 1
- EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zerostatement · cited by 1
- SummationFilter.tprod_symmetricIcc_eq_tprod_symmetricIcostatement · cited by 0
- SummationFilter.hasProd_symmetricIco_int_iffstatement · cited by 0