English
If a collection g of subsets is such that the σ-algebra generated from g contains exactly the sets in g, then the constructed space mkOfClosure g hg equals the generated sigma-algebra generateFrom g.
Русский
Если множество g подмножеств обладает тем свойством, что порожденная сигма-алгебра совпадает с g, то сконструированное пространство mkOfClosure g hg равно generateFrom g.
LaTeX
$$$\\text{MeasurableSpace.mkOfClosure}(g,hg) = \\text{MeasurableSpace.generateFrom}(g)$$$
Lean4
/-- If `g` is a collection of subsets of `α` such that the `σ`-algebra generated from `g` contains
the same sets as `g`, then `g` was already a `σ`-algebra. -/
protected def mkOfClosure (g : Set (Set α)) (hg : {t | MeasurableSet[generateFrom g] t} = g) : MeasurableSpace α :=
(generateFrom g).copy (· ∈ g) <| Set.ext_iff.1 hg.symm
