isSeqClosed_iff_isClosed — Mathlib

English

In a sequential space, a set is sequentially closed iff it is closed.

Русский

В последовательном пространстве множество последовательнозамкнуто тогда и только тогда замкнуто.

LaTeX

$$$IsSeqClosed M \iff IsClosed M$$$

Lean4

/-- In a sequential space, a set is closed iff it's sequentially closed. -/
theorem isSeqClosed_iff_isClosed [SequentialSpace X] {M : Set X} : IsSeqClosed M ↔ IsClosed M :=
  ⟨IsSeqClosed.isClosed, IsClosed.isSeqClosed⟩

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