isClosed — Mathlib

English

In a sequential space, every sequentially closed set is closed.

Русский

В последовательном пространстве любая последовательностно замкнутая множества является замкнутой.

LaTeX

$$$[\\text{SequentialSpace } X] \\Rightarrow (\\text{IsSeqClosed}(S) \\to \\text{IsClosed}(S))$$$

Lean4

/-- In a sequential space, a sequentially closed set is closed. -/
protected theorem isClosed [SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) : IsClosed s :=
  SequentialSpace.isClosed_of_seq s hs

Похожие утверждения