English
A subset s of X is constructible if it lies in the Boolean subalgebra generated by open retrocompact sets; equivalently, it can be built from open retrocompact sets using finite unions, finite intersections, and complements.
Русский
Подмножество s пространства X конструктивно, если оно лежит в булловой подалгебре, порождённой открытыми ретрокомпактными множествами; эквивалентно — строится из открытых ретрокомпактных множеств с помощью конечных объединений, пересечений и дополнений.
LaTeX
$$IsConstructible(s) ↔ s ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U}$$
Lean4
/-- A constructible set is a set that can be written as the
finite union/finite intersection/complement of open retrocompact sets.
In other words, constructible sets form the Boolean subalgebra generated by open retrocompact sets.
-/
def IsConstructible (s : Set X) : Prop :=
s ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U}
