Theorem LinearOrder.bot_topologicalSpace_eq_preorderTopology

Modification history

2026-04-15 06:19
Mathlib/Topology/Instances/Discrete.lean
chore(Topology/Order/Basic): use `Preorder.topology` in `OrderTopology` (#36958) …
Added LinearOrder.bot_topologicalSpace_eq_preorderTopologyView on Github →