measure_eq_iSup_isClosed_of_ne_top

English

For a measurable set A, there is a closed F ⊆ A with μ(A\F) small when μ(A) is finite.

Русский

Для измеримого множества A существует замкнутое F ⊆ A с малой мерой различия A\F, если μ(A) конечна.

LaTeX

$$$A\text{ measurable},\ μ(A) < ∞ \Rightarrow ∃ F\subseteq A:\ IsClosed F \land μ(A\setminus F) < ε$$$

Lean4

/-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
inside by closed sets. -/
theorem _root_.MeasurableSet.measure_eq_iSup_isClosed_of_ne_top [WeaklyRegular μ] ⦃A : Set α⦄ (hA : MeasurableSet A)
    (h'A : μ A ≠ ∞) : μ A = ⨆ (K) (_ : K ⊆ A) (_ : IsClosed K), μ K :=
  innerRegular_measurable.measure_eq_iSup ⟨hA, h'A⟩

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