Mathlib Map

Theorems · Theorem · sequences and series

Multipliable.finite_mulSupport_of_discreteTopology

Deprecated since 2026-03-03Use Multipliable.hasFiniteMulSupport_of_discreteTopology instead.

∀ {α : Type u_5} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α),
  Multipliable f → Function.HasFiniteMulSupport f

Alias of Multipliable.hasFiniteMulSupport_of_discreteTopology.

Defined in
Mathlib.Topology.Algebra.InfiniteSum.Group
Cited by
0 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommGroupTopologicalSpaceDiscreteTopology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TopologicalSpace · cited by 24529TopologicalSpaceSummationFilter.unconditional · cited by 2068SummationFilter.unconditi…CommGroup · cited by 990CommGroupDiscreteTopology · cited by 373DiscreteTopologyMultipliable · cited by 213MultipliableFunction.HasFiniteMulSupport · cited by 99Function.HasFiniteMulSupp…Multipliable.hasFiniteMulSupport_of_discreteTopology · cited by 1Multipliable.hasFiniteMul…Multipliable.finite_mulSuppor…CITED BYCITES

Cites7

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.