α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
hx : NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ 𝓝[{x}ᶜ] x = ⊥
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
hx : NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : s ∈ 𝓝 x
⊢ Set.Infinite s
refine' fun hsf => hx.1 _
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
hx : NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ IsOpen {x}
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
hx : NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ 𝓝[{x}ᶜ] x = ⊥
rw [← isOpen_singleton_iff_punctured_nhds]
no goals
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
hx : NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ IsOpen {x}
exact isOpen_singleton_of_finite_mem_nhds x hs hsf