Priestley spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source

@[class]

structure priestley_space (α : Type u_2) [preorder α] [topological_space α] :

Type

priestley : ∀ {x y : α}, ¬x ≤ y → (∃ (U : set α), is_clopen U ∧ is_upper_set 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.

Instances for priestley_space

priestley_space.has_sizeof_inst

source

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)

source

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

source

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

source

@[protected, instance]

def priestley_space.to_t2_space {α : Type u_1} [topological_space α] [partial_order α] [priestley_space α] :

t2_space α