Documentation

Mathlib.Topology.Order.Priestley

Priestley spaces #

This file defines Priestley spaces. A Priestley space is an ordered compact topological space such that any two distinct points can be separated by a clopen upper set.

Main declarations #

Implementation notes #

We do not include compactness in the definition, so a Priestley space is to be declared as follows: [Preorder α] [TopologicalSpace α] [CompactSpace α] [PriestleySpace α]

References #

class PriestleySpace (α : Type u_2) [Preorder α] [TopologicalSpace α] :

A Priestley space is an ordered topological space such that any two distinct points can be separated by a clopen upper set. Compactness is often assumed, but we do not include it here.

Instances
    theorem exists_clopen_upper_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x : α} {y : α} :
    ¬x yU, IsClopen U IsUpperSet U x U ¬y U
    theorem exists_clopen_lower_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x : α} {y : α} (h : ¬x y) :
    U, IsClopen U IsLowerSet U ¬x U y U
    theorem exists_clopen_upper_or_lower_of_ne {α : Type u_1} [TopologicalSpace α] [PartialOrder α] [PriestleySpace α] {x : α} {y : α} (h : x y) :