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][davey_priestley]

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

• priestley : ∀ {x y : α}, ¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ ¬y ∈ U

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.

theorem exists_clopen_upper_of_not_le {α : Type u_1} [TopologicalSpace α] [Preorder α] [PriestleySpace α] {x : α} {y : α} : ¬x ≤ y → ∃ U, 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) : ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U

instance PriestleySpace.toT2Space {α : Type u_1} [TopologicalSpace α] [PartialOrder α] [PriestleySpace α] : T2Space α