ae_isMeasurablyGenerated — Mathlib

English

The almost everywhere σ-algebra ae μ is generated by a countable family of sets.

Русский

Система AE-мера ae μ является счетно порожденной сигма-алгеброй.

LaTeX

$$$$\\text{IsMeasurablyGenerated}(\\mathrm{ae}\\,\\mu).$$$$

Lean4

instance ae_isMeasurablyGenerated : IsMeasurablyGenerated (ae μ) :=
  ⟨fun _s hs =>
    let ⟨t, hst, htm, htμ⟩ := exists_measurable_superset_of_null hs
    ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩

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