English
Let X be a topological space with an Alexandrov upper-set topology coming from a preorder. For each x in X, the principal open set P(x) := { y in X | x ≤ y } is an open subset of X, and the assignment x ↦ P(x) defines a contravariant functor X → Opens(X).
Русский
Пусть X — топологическое пространство с топологией Александрова, задаваемой сверху с помощью предорядка. Для каждого x ∈ X множество P(x) := { y ∈ X | x ≤ y } является открытым подмножеством X, и отображение x ↦ P(x) образует контравариантный функтор X → Opens(X).
LaTeX
$$$\operatorname{principalOpen}(x) = \{ y \in X \mid x \le y \}$$$
Lean4
/-- Given `x : X`, this is the principal open subset of `X` generated by `x`. -/
def principalOpen (x : X) : Opens X :=
.mk {y | x ≤ y} <| by
rw [IsUpperSet.isOpen_iff_isUpperSet]
intro y z h1 h2
exact le_trans h2 h1
