Mathlib Map

Theorems · Theorem · sequences and series

SummableUniformly.hasSumUniformly

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  SummableUniformly f → HasSumUniformly f fun x => ∑' (i : ι), f i x
Defined in
Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Cited by
1 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoidUniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

summableUniformly_iff_hasSumUniformly · cited by 0summableUniformly_iff_has…AddCommMonoid · cited by 12281AddCommMonoidSummationFilter.unconditional · cited by 2068SummationFilter.unconditi…UniformSpace · cited by 2040UniformSpacetsum · cited by 1148tsumHasSumUniformly · cited by 12HasSumUniformlySummableUniformly · cited by 7SummableUniformlySummableUniformlyOn.hasSumUniformlyOn · cited by 4SummableUniformlyOn.hasSu…hasSumUniformlyOn_univ_iff · cited by 2hasSumUniformlyOn_univ_iffsummableUniformlyOn_univ_iff · cited by 1summableUniformlyOn_univ_…SummableUniformly.hasSumUnifo…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.