Theorems · Theorem · sequences and series
Summable.indicator
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
[CompleteSpace α], Summable f → ∀ (s : Set β), Summable (s.indicator f)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommGroupstatement and proof · cited by 12,871
- CompleteSpacestatement and proof · cited by 2,532
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- UniformSpacestatement and proof · cited by 2,040
- Summablestatement and proof · cited by 778
- Set.indicatorstatement · cited by 723
- IsUniformAddGroupstatement and proof · cited by 342
- Set.indicator_eq_zero_or_selfproof · cited by 2
- Summable.summable_of_eq_zero_or_selfproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- Summable.comp_injectiveproof · cited by 22
- ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_oneproof · cited by 2
- not_summable_one_div_on_primesproof · cited by 2
- LSeries.tendsto_cpow_mul_atTopproof · cited by 2
- ArithmeticFunction.not_LSeriesSummable_moebius_at_oneproof · cited by 1
- summable_indicator_mod_iffproof · cited by 1
- tsum_geometric_inv_two_geproof · cited by 0