Theorems · Theorem · sequences and series

Set.Finite.of_summable_const

∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α},
  0 < b → (Summable fun x => b) → Set.univ.Finite

Defined in: Mathlib.Topology.Algebra.InfiniteSum.Order
Cited by: 1 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup LinearOrder IsOrderedAddMonoid TopologicalSpace Archimedean OrderClosedTopology

Mathlib docs Source Loogle LeanSearch

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.

TopologicalSpacestatement and proof · cited by 24,529
AddCommGroupstatement and proof · cited by 12,871
LinearOrderstatement and proof · cited by 8,572
Set.univstatement · cited by 3,945
SummationFilter.unconditionalstatement and proof · cited by 2,068
Set.Finitestatement · cited by 1,814
IsOrderedAddMonoidstatement and proof · cited by 1,659
Summablestatement and proof · cited by 778
Archimedeanstatement and proof · cited by 603
OrderClosedTopologystatement and proof · cited by 445
Set.finite_univ_iffproof · cited by 10
Finite.of_summable_constproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

memℓp_genproof · cited by 8