mathlib documentation

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

References #

@[class]
structure priestley_space (α : Type u_2) [preorder α] [topological_space α] :
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} [topological_space α] [preorder α] [priestley_space α] {x y : α} :
¬x y(∃ (U : set α), is_clopen U is_upper_set U x U y U)
theorem exists_clopen_lower_of_not_le {α : Type u_1} [topological_space α] [preorder α] [priestley_space α] {x y : α} (h : ¬x y) :
∃ (U : set α), is_clopen U is_lower_set U x U y U
theorem exists_clopen_upper_or_lower_of_ne {α : Type u_1} [topological_space α] [partial_order α] [priestley_space α] {x y : α} (h : x y) :
∃ (U : set α), is_clopen U (is_upper_set U is_lower_set U) x U y U
@[protected, instance]