no goals
α : Type u
β : Type v
γ : Type ?u.39116
f : α → β
ι : Sort ?u.39123
T : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ (t : TopologicalSpace α), t ∈ T → Continuous f
simp only [continuous_iff_le_induced, sSup_le_iff]