fin_meas — Mathlib

English

If 𝒜 is measure-dense, then for any measurable s there exists t∈𝒜 with μ(s Δ t) arbitrarily small and μ t finite.

Русский

Если 𝒜 плотна в плане меры, то можно подобрать t ∈ 𝒜 так, чтобы μ(s Δ t) было произвольно маленьким и μ t сколь угодно конечна.

LaTeX

$$$ \\exists t ∈ 𝒜, μ t ≠ ∞ ∧ μ (s Δ t) < ε $$$

Lean4

/-- If a family of sets `𝒜` is measure-dense in `X`, then it is also the case for the sets in `𝒜`
with finite measure. -/
theorem fin_meas (h𝒜 : μ.MeasureDense 𝒜) : μ.MeasureDense {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
    where
  measurable s h := h𝒜.measurable s h.1
  approx s ms hμs ε
    ε_pos := by
    rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩
    exact ⟨t, ⟨t_mem, hμt⟩, hμst⟩

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