no goals
α : Type u
β : Type v
γ : Type u_1
f : α → β
ι : Sort ?u.36895
g : γ → α
t₂ : TopologicalSpace β
t₁ : TopologicalSpace γ
⊢ Continuous g ↔ Continuous (f ∘ g)
simp only [continuous_iff_le_induced, induced_compose]