isCompact_closure_singleton — Mathlib

English

In an R0 space, the closure of a singleton is compact.

Русский

В R0-пространстве замыкание единичного множества компактно.

LaTeX

$$$\\operatorname{IsCompact}(\\overline{\\{x\\}})$$$

Lean4

/-- In an R₀ space, the closure of a singleton is a compact set. -/
theorem isCompact_closure_singleton : IsCompact (closure { x }) :=
  by
  refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_
  obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl
  refine ⟨{ i }, fun y hy ↦ ?_⟩
  rw [← specializes_iff_mem_closure, specializes_comm] at hy
  simpa using hy.mem_open (hUo i) hi

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