closure_eq_biUnion_closure_singleton

English

In an R1 space, the closure of a compact set K is the union of the closures of its points: cl(K) = ⋃_{x ∈ K} cl({x}).

Русский

В пространстве R1 замыкание компактного множества K является объединением замыканий его точек: \overline{K} = \bigcup_{x \in K} \overline{\{x\}}.

LaTeX

$$$IsCompact(closure(K)) =? IsCompact(closure(K))$$$

Lean4

/-- In an R₁ space, the closure of a compact set is the union of the closures of its points. -/
theorem closure_eq_biUnion_closure_singleton {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, closure { x } := by
  simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable, specializes_iff_mem_closure,
    setOf_mem_eq]

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