no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.350648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
simp_rw [ContinuousOn, hg.continuousWithinAt_iff]