MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Topology.exists_isOpen_singleton

Raw UTF-8 source

theorem exists_isOpen_singleton [Nonempty X] [Countable X] [T1Space X]
    [BaireSpace X] : ∃ x : X, IsOpen ({x} : Set X)

1 import Mathlib.Topology.Baire.Lemmas
2 import Mathlib.Topology.Separation.Basic
3 
4 /-!
5 # Isolated points in countable Baire spaces
6 -/
7 
8 set_option autoImplicit false
9 
10 open Set
11 
12 namespace MathlibAnnex.Topology
13 
14 universe u
15 
16 variable {X : Type u} [TopologicalSpace X]
17 
18 /-- A nonempty countable T1 Baire space has an isolated point. -/
19 theorem exists_isOpen_singleton [Nonempty X] [Countable X] [T1Space X]
20     [BaireSpace X] : ∃ x : X, IsOpen ({x} : Set X) := by
21   obtain ⟨x, y, hy⟩ := nonempty_interior_of_iUnion_of_closed
22     (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 ▸ hy
27   refine ⟨x, interior_eq_iff_isOpen.mp ?_⟩
28   exact le_antisymm interior_subset (singleton_subset_iff.mpr hx)
29 
30 end MathlibAnnex.Topology