no goals
α : Type u
β : Type v
γ : Type ?u.39838
f : α → β
ι : Sort u_1
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ (i : ι), Continuous f
simp only [continuous_iff_le_induced, iSup_le_iff]