IsSeqClosed.isClosed

theorem IsSeqClosed.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SequentialSpace X] {s : Set X}, IsSeqClosed s → IsClosed s

In the context of a sequential space, this theorem states that if a set is sequentially closed, it is also a closed set. To elaborate, given a set `s` in a topological space `X` that also has a sequential space structure, if for any sequence of elements in `s` that converges to a limit `p`, `p` is also an element of `s` (definition of `IsSeqClosed`), then `s` is a closed set in the topological sense (i.e., its complement is an open set).

More concisely: In a sequential space, a set is closed if and only if every convergent sequence in the set limits to an element in the set.