exists_isClopen_upper_of_not_le — Mathlib

English

In a Priestley space, if x not ≤ y, there exists a clopen upper set U with x ∈ U and y ∉ U.

Русский

В Priestley-пространстве, если не x ≤ y, существует открыто-душевное (clopen) верхнее множество U такое, что x ∈ U и y ∉ U.

LaTeX

$$$\\lnot x \\le y \\Rightarrow \\exists U: Set\\;\\alpha,\\ IsClopen U \\land IsUpperSet U \\land x\\in U \\land y\\notin U.$$$

Lean4

theorem exists_isClopen_upper_of_not_le : ¬x ≤ y → ∃ U : Set α, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U :=
  PriestleySpace.priestley

Похожие утверждения