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 PriestleySpace.priestley {α : Type u_2} :
    ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : PriestleySpace α] {x y : α}, ¬x y∃ (U : Set α), IsClopen U IsUpperSet U x U yU
    theorem exists_isClopen_upper_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x : α} {y : α} :
    ¬x y∃ (U : Set α), IsClopen U IsUpperSet U x U yU
    theorem exists_isClopen_lower_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x : α} {y : α} (h : ¬x y) :
    ∃ (U : Set α), IsClopen U IsLowerSet U xU y U
    theorem exists_isClopen_upper_or_lower_of_ne {α : Type u_1} [TopologicalSpace α] [PartialOrder α] [PriestleySpace α] {x : α} {y : α} (h : x y) :
    ∃ (U : Set α), IsClopen U (IsUpperSet U IsLowerSet U) x U yU
    @[instance 100]
    Equations
    • =