chore(topology/order): open function, don't open classical (#16288)

src/topology/order.lean

@@ -41,7 +41,7 @@ finer, coarser, induced topology, coinduced topology
 
 -/
 
-open set filter classical
+open function set filter
 open_locale classical topological_space filter
 
 universes u v w
@@ -189,16 +189,14 @@ lemma generate_from_set_of_is_open (t : topological_space α) :
 (gi_generate_from α).l_u_eq t
 
 lemma left_inverse_generate_from :
-  function.left_inverse topological_space.generate_from
-    (λ t : topological_space α, {s | t.is_open s}) :=
+  left_inverse topological_space.generate_from (λ t : topological_space α, {s | t.is_open s}) :=
 (gi_generate_from α).left_inverse_l_u
 
 lemma generate_from_surjective :
-  function.surjective (topological_space.generate_from : set (set α) → topological_space α) :=
+  surjective (topological_space.generate_from : set (set α) → topological_space α) :=
 (gi_generate_from α).l_surjective
 
-lemma set_of_is_open_injective :
-  function.injective (λ t : topological_space α, {s | t.is_open s}) :=
+lemma set_of_is_open_injective : injective (λ t : topological_space α, {s | t.is_open s}) :=
 (gi_generate_from α).u_injective
 
 /-- The "temporary" order `tmp_order` on `topological_space α`, i.e. the inclusion order, is a
@@ -738,7 +736,7 @@ tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 $ f b) :=
 ⟨λ h a, h.symm ▸ nhds_induced f a, λ h, eq_of_nhds_eq_nhds $ λ x, by rw [h, nhds_induced]⟩
 
 theorem map_nhds_induced_of_surjective [T : topological_space α]
-    {f : β → α} (hf : function.surjective f) (a : β) :
+    {f : β → α} (hf : surjective f) (a : β) :
   map f (@nhds β (topological_space.induced f T) a) = 𝓝 (f a) :=
 by rw [nhds_induced, map_comap_of_surjective hf]