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