English
The smallest sigma-algebra on α containing a given family s of subsets is defined as GenerateFrom s, with measurability determined by GenerateMeasurable s and the closure properties empty, complement, and countable unions.
Русский
На множестве α определяется наименьшая сигма-алгебра, содержащая данную коллекцию s подмножеств; она определяется как GenerateFrom s, где множество измеримых принимает GenerateMeasurable s, и выполняются замыкания: пустое множество, дополнение и счетные объединения.
LaTeX
$$$\\text{generateFrom}(s)$ is the MeasurableSpace on $\\alpha$ with$$\\text{MeasurableSet}' = \\text{GenerateMeasurable}(s),\\; \\emptyset, \\text{compl}, \\text{iUnion}.$$$$
Lean4
/-- Construct the smallest measure space containing a collection of basic sets -/
def generateFrom (s : Set (Set α)) : MeasurableSpace α
where
MeasurableSet' := GenerateMeasurable s
measurableSet_empty := .empty
measurableSet_compl := .compl
measurableSet_iUnion := .iUnion
