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