α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ IsOpen {b}
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
⊢ IsOpen {b}
letI := nhdsAdjoint a f
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ IsOpen {b}
rw [isOpen_singleton_iff_nhds_eq_pure]
no goals
α✝ : Type u
β : Type v
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
exact nhdsAdjoint_nhds_of_ne a f hb