English
The upper topology on a preorder α is the coarsest topology for which all sets of the form { x : x ≤ a }^c are open, i.e., generated by the complements of right-closed rays.
Русский
Верхняя топология на преддолжимом множество α — наименьшая топология, для которой все множества вида (Iic a)^c открыты, то есть топология, генерируемая комплементами правозакрытых лучей.
LaTeX
$$$\\tau_{\\mathrm{up}}(\\alpha) = \\sigma\\bigl\\{ (\\Iic a)^{c} : a \\in \\alpha \\bigr\\}$$$
Lean4
/-- The upper topology is the topology generated by the complements of the right-closed left-infinite
intervals.
-/
def upper (α : Type*) [Preorder α] : TopologicalSpace α :=
generateFrom {s | ∃ a, (Iic a)ᶜ = s}
