Theorems · Definition · general topology

Preorder.topology

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

(Order) topology on a partial order α generated by the subbase of open intervals (a, ∞) = { x ∣ a < x }, (-∞, b) = {x ∣ x < b} for all a, b in α. We do not register it as an instance as many ordered sets are already endowed with the same topology, most often in a non-defeq way though. Register as a local instance when necessary.

Defined in

Mathlib.Topology.Order.Basic

Cited by

24 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Preorder