English
For distinct x ≠ y in a Priestley space, there exists a clopen set U containing x but not y, and U is either upper or lower.
Русский
Для различных x ≠ y в Priestley-пространстве существует clopen множество U с x ∈ U, y ∉ U, и U либо верхнее, либо нижнее.
LaTeX
$$$\\forall x\\neq y,\\ \\exists U,\\ IsClopen U \\land (IsUpperSet U \\lor IsLowerSet U) \\land x\\in U \\land y\\notin U.$$$
Lean4
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_ge
· 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⟩
-- See note [lower instance priority]
