Theorems · Theorem · sequences and series
summable_of_hasFiniteSupport
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
{L : SummationFilter β} [L.HasSupport], Function.HasFiniteSupport f → Summable f L- Cited by
- 12 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommMonoidstatement and proof · cited by 12,281
- Summablestatement · cited by 778
- SummationFilterstatement and proof · cited by 607
- Function.HasFiniteSupportstatement and proof · cited by 113
- Set.Finite.mem_toFinsetproof · cited by 74
- Function.mem_supportproof · cited by 54
- SummationFilter.HasSupportstatement and proof · cited by 38
- summable_of_ne_finset_zeroproof · cited by 4
Cited by12
Results whose statement or proof uses this declaration.
- tsum_eq_finsumproof · cited by 4
- Summable.of_finiteproof · cited by 4
- PeriodPair.weierstrassPExcept_addproof · cited by 3
- PeriodPair.coeff_weierstrassPExceptSeriesproof · cited by 3
- Nat.infinite_setOfPred_prime_and_eq_modproof · cited by 2
- PeriodPair.derivWeierstrassPExcept_subproof · cited by 1
- PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_topproof · cited by 1
- PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_topproof · cited by 1
- FormalMultilinearSeries.changeOrigin_eval_of_finiteproof · cited by 1
- summable_of_finite_supportproof · cited by 0