# 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 #

• PriestleySpace: Prop-valued mixin stating the Priestley separation axiom: Any two distinct points can be separated by a clopen upper set.

## 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) [] [] :

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} [] [] [self : ] {x : α} {y : α} :
¬x y∃ (U : Set α), x U yU
theorem exists_isClopen_upper_of_not_le {α : Type u_1} [] [] [] {x : α} {y : α} :
¬x y∃ (U : Set α), x U yU
theorem exists_isClopen_lower_of_not_le {α : Type u_1} [] [] [] {x : α} {y : α} (h : ¬x y) :
∃ (U : Set α), xU y U
theorem exists_isClopen_upper_or_lower_of_ne {α : Type u_1} [] [] [] {x : α} {y : α} (h : x y) :
∃ (U : Set α), () x U yU
@[instance 100]
instance PriestleySpace.toT2Space {α : Type u_1} [] [] [] :
Equations
• =