Mathlib Map

Theorems · Theorem · sequences and series

Set.Finite.summable_compl_iff

∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {s : Set β}, s.Finite → (Summable (f ∘ Subtype.val) ↔ Summable f)
Defined in
Mathlib.Topology.Algebra.InfiniteSum.Group
Cited by
2 results in Mathlib
Foundations
Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupTopologicalSpaceIsTopologicalAddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Summable.congr_cofinite · cited by 5Summable.congr_cofinitesummable_indicator_mod_iff_summable · cited by 2summable_indicator_mod_if…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceAddCommGroup · cited by 12871AddCommGroupSet.Elem · cited by 7166Set.ElemCompl.compl · cited by 2925Compl.complSummationFilter.unconditional · cited by 2068SummationFilter.unconditi…Set.Finite · cited by 1814Set.FiniteIsTopologicalAddGroup · cited by 1394IsTopologicalAddGroupSummable · cited by 778SummableSummable.summable_compl_iff · cited by 2Summable.summable_compl_i…Set.Finite.summable · cited by 2Finite.summableFinite.summable_compl_iffCITED BYCITES

Cites11

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

Cited by2

Results whose statement or proof uses this declaration.