Theorems · Theorem · sequences and series
tsum_subtype
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β) (f : β → α),
∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x- Cited by
- 6 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommMonoidstatement and proof · cited by 12,281
- Set.Elemstatement and proof · cited by 7,166
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- tsumstatement and proof · cited by 1,148
- Set.indicatorstatement and proof · cited by 723
- Set.indicator_of_memproof · cited by 161
- tsum_congrproof · cited by 64
- Subtype.coe_propproof · cited by 42
- tsum_subtype_eq_of_support_subsetproof · cited by 7
- Set.support_indicator_subsetproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- not_summable_one_div_on_primesproof · cited by 2
- MeasureTheory.Measure.map_eq_sumproof · cited by 1
- MeasureTheory.Measure.le_count_applyproof · cited by 1
- Nat.Primes.tsum_eq_tsum_iteproof · cited by 0
- ENNReal.sum_add_tsum_complproof · cited by 0
- MeasureTheory.Measure.sum_restrict_leproof · cited by 0