Exact source: MathlibAnnex/Topology/CountableBaire.lean
Pinned GitHub source · Raw UTF-8 source
Back to An isolated character away from the scalar character · Back to An isolated point in a countable Baire space
1import Mathlib.Topology.Baire.Lemmas2import Mathlib.Topology.Separation.Basic34/-!5# Isolated points in countable Baire spaces6-/78set_option autoImplicit false910open Set1112namespace MathlibAnnex.Topology1314universe u1516variable {X : Type u} [TopologicalSpace X]1718/-- A nonempty countable T1 Baire space has an isolated point. -/19theorem exists_isOpen_singleton [Nonempty X] [Countable X] [T1Space X]20 [BaireSpace X] : ∃ x : X, IsOpen ({x} : Set X) := by21 obtain ⟨x, y, hy⟩ := nonempty_interior_of_iUnion_of_closed22 (f := fun x : X => ({x} : Set X))23 (fun _ => isClosed_singleton)24 (by ext y; simp)25 have hyx : y = x := mem_singleton_iff.mp (interior_subset hy)26 have hx : x ∈ interior ({x} : Set X) := hyx ▸ hy27 refine ⟨x, interior_eq_iff_isOpen.mp ?_⟩28 exact le_antisymm interior_subset (singleton_subset_iff.mpr hx)2930end MathlibAnnex.Topology