completion — Mathlib

English

If μ is generated by an algebra 𝒜 of sets and 𝒜 is measure-dense, then μ is measure-dense on 𝒜.

Русский

Если μ порождается алгеброй 𝒜 и 𝒜 плотна по мере, то μ плотна по 𝒜.

LaTeX

$$$ (\\text{IsFiniteMeasure } μ) \\Rightarrow μ.MeasureDense 𝒜 \\rightarrow \\n$$

Lean4

theorem completion (h𝒜 : μ.MeasureDense 𝒜) : μ.completion.MeasureDense 𝒜
    where
  measurable s hs := (h𝒜.measurable s hs).nullMeasurableSet
  approx s hs hμs ε
    ε_pos :=
    by
    obtain ⟨t, ht, hμst⟩ := h𝒜.approx (toMeasurable μ s) (measurableSet_toMeasurable μ s) (by simpa) ε ε_pos
    refine ⟨t, ht, ?_⟩
    convert hμst using 1
    rw [completion_apply]
    exact measure_congr <| ae_eq_set_symmDiff (NullMeasurableSet.toMeasurable_ae_eq hs).symm Filter.EventuallyEq.rfl

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