no goals
α : Type u
β : Type v
γ : Type ?u.40406
f : α → β
ι : Sort ?u.40413
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f
simp only [continuous_iff_coinduced_le, le_inf_iff]