Theorems · Inductive type · general topology

OrderClosedTopology

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

A topology on a set which is both a topological space and a preorder is _order-closed_ if the set of points (x, y) with x ≤ y is closed in the product space. We introduce this as a mixin. This property is satisfied for the order topology on a linear order, but it can be satisfied more generally, and suffices to derive many interesting properties relating order and topology.

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

445 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorder