English
Let α be a preorder. The family of subsets s ⊆ α that arise as the complement of the upper closure of a finite set t forms a basis for the lower topology on α.
Русский
Пусть α упорядочено частично. Семейство подмножеств s ⊆ α, которые являются дополнениями к верхним окрестностям конечных множеств t, образуют базис нижней топологии на α.
LaTeX
$$$\\text{lowerBasis}(\\alpha) = \\{ s \\subseteq \\alpha \\mid \\exists t \\subseteq \\alpha,\\ t \\text{ finite} \\land (\\operatorname{upperClosure}(t))^{c} = s \\}$$$
Lean4
/-- The complements of the upper closures of finite sets are a collection of lower sets
which form a basis for the lower topology. -/
def lowerBasis (α : Type*) [Preorder α] :=
{s : Set α | ∃ t : Set α, t.Finite ∧ (upperClosure t : Set α)ᶜ = s}
