no goals
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhds_left_sup_nhds_right]