no goals
α : Type u
β : Type v
γ : Type ?u.38234
f : α → β
ι : Sort ?u.38241
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f
simp only [continuous_iff_le_induced, sup_le_iff]