Structures · Topology

OrderTopology

The order topology on an ordered type is the topology generated by open intervals. We register it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed. We define it as a mixin. If you want to introduce the order topology on a preorder, use Preorder.topology.

Defined in

Mathlib.Topology.Order.Basic

Shape

One type argument · adds topology_eq_generate_intervals