mathlib3

c83488b9 - feat(topology/order/priestley): Priestley spaces (#12044)

feat(topology/order/priestley): Priestley spaces (#12044) Define `priestley_space`, a Prop-valued mixin for an ordered topological space to respect Priestley's separation axiom.