# mathlibdocumentation

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 #

• priestley_space: 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 α] [topological_space α] [compact_space α] [priestley_space α]

## References #

@[class]
structure priestley_space (α : Type u_2) [preorder α]  :
Type

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 for priestley_space
• priestley_space.has_sizeof_inst
theorem exists_clopen_upper_of_not_le {α : Type u_1} [preorder α] {x y : α} :
¬x y(∃ (U : set α), x U y U)
theorem exists_clopen_lower_of_not_le {α : Type u_1} [preorder α] {x y : α} (h : ¬x y) :
∃ (U : set α), x U y U
theorem exists_clopen_upper_or_lower_of_ne {α : Type u_1} {x y : α} (h : x y) :
∃ (U : set α), x U y U
@[protected, instance]
def priestley_space.to_t2_space {α : Type u_1}  :