no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.138402
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : QuotientMap f
⊢ Continuous g ↔ Continuous (g ∘ f)
rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.right, coinduced_compose]