no goals
α : Type u_1
β : Type u_2
γ : Type ?u.322097
δ : Type ?u.322100
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x
simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]