Theorems · Inductive type · general topology

OrderTopology

(α : Type u_1) → [t : TopologicalSpace α] → [Preorder α] → Prop

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

Cited by

1,355 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpacePreorder