English
The smallest topology on a set α containing a family g of subsets is generated by declaring as open exactly the sets that can be formed by finite unions and intersections of elements of g, including arbitrary unions.
Русский
На множестве α задана наименьшая топология, содержащая семейство подмножеств g; открытыми являются множества, получаемые конечными объединениями/пересечениями элементов g и произвольными объединениями.
LaTeX
$$$\\text{generateFrom}(g) \\text{ is the smallest topology on } \\alpha \\text{ containing } g.$$$
Lean4
/-- The smallest topological space containing the collection `g` of basic sets -/
def generateFrom (g : Set (Set α)) : TopologicalSpace α
where
IsOpen := GenerateOpen g
isOpen_univ := GenerateOpen.univ
isOpen_inter := GenerateOpen.inter
isOpen_sUnion := GenerateOpen.sUnion
