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

• Wikipedia, Priestley space
• Davey, Priestley Introduction to Lattices and Order

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

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.

• priestley {x y : α} : ¬x ≤ y → ∃ (U : Set α), IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U

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 ∧ y ∉ U

theorem exists_isClopen_lower_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x y : α} (h : ¬x ≤ y) : ∃ (U : Set α), IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ 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 ∧ y ∉ U

@[instance 100]

instance PriestleySpace.toTotallySeparatedSpace {α : Type u_1} [TopologicalSpace α] [PartialOrder α] [PriestleySpace α] : TotallySeparatedSpace α