fix

JovanGerb · JovanGerb · commit efcfeba27d6a · 2026-03-22T03:10:59.000Z
diff --git a/Mathlib/Topology/Instances/Discrete.lean b/Mathlib/Topology/Instances/Discrete.lean
@@ -42,16 +42,20 @@ instance (priority := 100) DiscreteTopology.secondCountableTopology_of_countable
     (iUnion_of_singleton α)
 
 set_option backward.isDefEq.respectTransparency false in
-theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α} [LinearOrder α] [PredOrder α]
-    [SuccOrder α] : (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } := by
+theorem LinearOrder.bot_topologicalSpace_eq_preorderTopology {α} [LinearOrder α] [PredOrder α]
+    [SuccOrder α] : (⊥ : TopologicalSpace α) = Preorder.topology α := by
   let _ := Preorder.topology α
   have : OrderTopology α := ⟨rfl⟩
   exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm
 
+@[deprecated (since := "2026-03-22")]
+alias LinearOrder.bot_topologicalSpace_eq_generateFrom :=
+  LinearOrder.bot_topologicalSpace_eq_preorderTopology
+
 theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOrder α]
     [SuccOrder α] : DiscreteTopology α ↔ OrderTopology α := by
   refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
-  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom]
+  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]
 
 instance OrderTopology.of_discreteTopology [LinearOrder α] [PredOrder α] [SuccOrder α]
     [DiscreteTopology α] : OrderTopology α :=
