Priestley

📁 Source: Mathlib/Topology/Order/Priestley.lean

Statistics

Metric	Count
Definitions PriestleySpace	1
Theorems priestley, toTotallySeparatedSpace, exists_isClopen_lower_of_not_le, exists_isClopen_upper_of_not_le, exists_isClopen_upper_or_lower_of_ne	5
Total	6

PriestleySpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
priestley 📖	mathematical	Preorder.toLE	IsClopen IsUpperSet Set Set.instMembership	—	—
toTotallySeparatedSpace 📖	mathematical	—	TotallySeparatedSpace	—	exists_isClopen_upper_or_lower_of_ne IsClopen.isOpen IsClopen.compl subset_rfl Set.instReflSubset Set.union_compl_self disjoint_compl_right

(root)

Definitions

Name	Category	Theorems
PriestleySpace 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isClopen_lower_of_not_le 📖	mathematical	Preorder.toLE	IsClopen IsLowerSet Set Set.instMembership	—	exists_isClopen_upper_of_not_le IsClopen.compl IsUpperSet.compl
exists_isClopen_upper_of_not_le 📖	mathematical	Preorder.toLE	IsClopen IsUpperSet Set Set.instMembership	—	PriestleySpace.priestley
exists_isClopen_upper_or_lower_of_ne 📖	mathematical	—	IsClopen IsUpperSet Preorder.toLE PartialOrder.toPreorder IsLowerSet Set Set.instMembership	—	Ne.not_le_or_not_ge exists_isClopen_upper_of_not_le exists_isClopen_lower_of_not_le

---

← Back to Index