Commit 2026-04-15 06:19 18538382

View on Github →

chore(Topology/Order/Basic): use Preorder.topology in OrderTopology (#36958) This PR addresses the comment:

TODO: define `Preorder.topology` before `OrderTopology` and reuse the def

Estimated changes

Modified Mathlib/Topology/Instances/Discrete.lean

deleted theorem LinearOrder.bot_topologicalSpace_eq_generateFrom

added theorem LinearOrder.bot_topologicalSpace_eq_preorderTopology

Modified Mathlib/Topology/Order/Basic.lean