no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
a✝ b✝ : α
inst✝ : TopologicalSpace γ
a b : α
f : α → γ
h : a < b
⊢ ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b
simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsWithin_Iio h]