exists_isClosed_diff_lt — Mathlib

English

For a measurable set s with finite measure, there exists an open U such that μ(U Δ s) is small.

Русский

Для измеримого множества s конечной меры существует открытое U, такое что μ(U Δ s) невелико.

LaTeX

$$$s\text{ measurable},\ μ(s) < ∞ \Rightarrow ∃ U:\ IsOpen(U) \land μ(U\Delta s) < ε$$$

Lean4

theorem _root_.MeasurableSet.exists_isClosed_diff_lt [OpensMeasurableSpace α] [WeaklyRegular μ] ⦃A : Set α⦄
    (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ F, F ⊆ A ∧ IsClosed F ∧ μ (A \ F) < ε :=
  by
  rcases hA.exists_isClosed_lt_add h'A hε with ⟨F, hFA, hFc, hF⟩
  exact
    ⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.nullMeasurableSet hFA (ne_top_of_le_ne_top h'A <| measure_mono hFA) hF⟩

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