Theorems · Theorem · sequences and series

tsum_mem

∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {ι : Type u_4} {S : Type u_5} {s : S}
  [inst_2 : SetLike S α] [AddSubmonoidClass S α],
  IsClosed ↑s → ∀ {f : ι → α}, (∀ (i : ι), f i ∈ s) → ∑' (i : ι), f i ∈ s

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Basic

Cited by

2 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpaceSetLikeAddSubmonoidClass