no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
a✝ b✝ : α
inst✝ : TopologicalSpace γ
a b : α
h : a < b
⊢ 𝓝[Ioo a b] b = 𝓝[Iio b] b
simpa only [dual_Ioo] using nhdsWithin_Ioo_eq_nhdsWithin_Ioi h.dual