fix(TopologicalSpace/Basic): restore curly braces in continuous_def (…

…#10110)

These were placed on purpose; reverting them caused breakage downstream.



Co-authored-by: grunweg <grunweg@posteo.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Topology/Basic.lean

@@ -1499,12 +1499,15 @@ variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalS
 
 open TopologicalSpace
 
-variable {f : X → Y} {s : Set X} {x : X} {y : Y}
-
-theorem continuous_def : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
+-- The curly braces are intentional, so this definition works well with simp
+-- when topologies are not those provided by instances.
+theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} :
+    Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
   ⟨fun hf => hf.1, fun h => ⟨h⟩⟩
 #align continuous_def continuous_def
 
+variable {f : X → Y} {s : Set X} {x : X} {y : Y}
+
 theorem IsOpen.preimage (hf : Continuous f) {t : Set Y} (h : IsOpen t) :
     IsOpen (f ⁻¹' t) :=
   hf.isOpen_preimage t h