generateMeasurableRec — Mathlib

English

The sigma-algebra generated by a collection s is constructed by transfinite recursion, starting from s and closing under countable unions and complements, and including the empty set.

Русский

Сигма-алгебра, порожденная множеством s, строится посредством трансфинитной рекурсии, начиная с s и замыкаясь на счетные объединения и дополнения, включая пустое множество.

LaTeX

$$$\\text{generateMeasurableRec}(s,i) = s\\cup\\{\\emptyset\\}\\cup\\operatorname{compl}''(\\bigcup_{j

Lean4

/-- Transfinite induction construction of the sigma-algebra generated by a set of sets `s`. At each
step, we add all elements of `s`, the empty set, the complements of already constructed sets, and
countable unions of already constructed sets.

We index this construction by an arbitrary ordinal for simplicity, but by `ω₁` we will have
generated all the sets in the sigma-algebra.

This construction is very similar to that of the Borel hierarchy. -/
def generateMeasurableRec (s : Set (Set α)) (i : Ordinal) : Set (Set α) :=
  let S := ⋃ j < i, generateMeasurableRec s j
  s ∪ {∅} ∪ compl '' S ∪ Set.range fun f : ℕ → S => ⋃ n, (f n).1
termination_by i

Похожие утверждения