fin_meas_approx — Mathlib

English

If 𝒜 is measure-dense, every measurable set of finite measure can be approximated by sets in 𝒜 with finite measure.

Русский

Если 𝒜 плотна, каждый измеримый набор с конечной мерой может быть аппроксимирован множествами из 𝒜 с конечной мерой.

LaTeX

$$$ \\exists t \\in 𝒜, \\mu t \\neq \\infty \\land \\mu (s \\Delta t) < \\mathrm{ENNReal.ofReal}(\\varepsilon) $$$

Lean4

/-- If a family of sets `𝒜` is measure-dense in `X`, then any measurable set with finite measure
can be approximated by sets in `𝒜` with finite measure. -/
theorem fin_meas_approx (h𝒜 : μ.MeasureDense 𝒜) {s : Set X} (ms : MeasurableSet s) (hμs : μ s ≠ ∞) (ε : ℝ)
    (ε_pos : 0 < ε) : ∃ t ∈ 𝒜, μ t ≠ ∞ ∧ μ (s ∆ t) < ENNReal.ofReal ε :=
  by
  rcases h𝒜.approx s ms hμs ε ε_pos with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, (measure_ne_top_iff_of_symmDiff <| ne_top_of_lt ht).1 hμs, ht⟩

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