no goals
α : Type u
β : Type v
γ : Type ?u.41516
f : α → β
ι : Sort ?u.41523
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous f ↔ ∀ (t : TopologicalSpace β), t ∈ T → Continuous f
simp only [continuous_iff_coinduced_le, le_sInf_iff]