-
Notifications
You must be signed in to change notification settings - Fork 259
/
Priestley.lean
82 lines (58 loc) · 3.07 KB
/
Priestley.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Order.UpperLower.Basic
import Mathlib.Topology.Separation
#align_import topology.order.priestley from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
/-!
# 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*](https://en.wikipedia.org/wiki/Priestley_space)
* [Davey, Priestley *Introduction to Lattices and Order*][davey_priestley]
-/
open Set
variable {α : 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. -/
class PriestleySpace (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
priestley {x y : α} : ¬x ≤ y → ∃ U : Set α, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U
#align priestley_space PriestleySpace
variable [TopologicalSpace α]
section Preorder
variable [Preorder α] [PriestleySpace α] {x y : α}
theorem exists_isClopen_upper_of_not_le :
¬x ≤ y → ∃ U : Set α, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U :=
PriestleySpace.priestley
#align exists_clopen_upper_of_not_le exists_isClopen_upper_of_not_le
theorem exists_isClopen_lower_of_not_le (h : ¬x ≤ y) :
∃ U : Set α, IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ y ∈ U :=
let ⟨U, hU, hU', hx, hy⟩ := exists_isClopen_upper_of_not_le h
⟨Uᶜ, hU.compl, hU'.compl, Classical.not_not.2 hx, hy⟩
#align exists_clopen_lower_of_not_le exists_isClopen_lower_of_not_le
end Preorder
section PartialOrder
variable [PartialOrder α] [PriestleySpace α] {x y : α}
theorem exists_isClopen_upper_or_lower_of_ne (h : x ≠ y) :
∃ U : Set α, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U := by
obtain h | h := h.not_le_or_not_le
· exact (exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
· obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h
exact ⟨U, hU, Or.inr hU', hx, hy⟩
#align exists_clopen_upper_or_lower_of_ne exists_isClopen_upper_or_lower_of_ne
-- See note [lower instance priority]
instance (priority := 100) PriestleySpace.toT2Space : T2Space α :=
⟨fun _ _ h ↦
let ⟨U, hU, _, hx, hy⟩ := exists_isClopen_upper_or_lower_of_ne h
⟨U, Uᶜ, hU.isOpen, hU.compl.isOpen, hx, hy, disjoint_compl_right⟩⟩
#align priestley_space.to_t2_space PriestleySpace.toT2Space
end PartialOrder