instIsMeasurablyGenerated — Mathlib

English

The cofinite σ-algebra μ.cofinite is generated by measurable sets; in particular μ.cofinite is is measurably generated.

Русский

Кофинитная сигма-алгебра μ.cofinite генерируется измеримыми множествами; то есть μ.cofinite является измеримо сгенерированной.

LaTeX

$$IsMeasurablyGenerated(μ.cofinite)$$

Lean4

instance instIsMeasurablyGenerated : IsMeasurablyGenerated μ.cofinite where
  exists_measurable_subset s
    hs := by
    refine ⟨(toMeasurable μ sᶜ)ᶜ, ?_, (measurableSet_toMeasurable _ _).compl, ?_⟩
    · rwa [compl_mem_cofinite, measure_toMeasurable]
    · rw [compl_subset_comm]
      apply subset_toMeasurable

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