isClosed — Mathlib

English

In a Hausdorff space, every compact set is closed.

Русский

В Хаусдорфовом пространстве всякое компактное множество замкнуто.

LaTeX

$$$[T2Space X] \\; s\\subset X, IsCompact s \\Rightarrow IsClosed s.$$$

Lean4

/-- In a `T2Space`, every compact set is closed. -/
@[aesop 50% apply, grind ←]
theorem isClosed [T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s :=
  isClosed_iff_forall_filter.2 fun _x _f _ hfs hfx =>
    let ⟨_y, hy, hfy⟩ := hs.exists_clusterPt hfs
    mem_of_eq_of_mem (eq_of_nhds_neBot (hfy.mono hfx).neBot).symm hy

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