exists_lt_isClosed_of_ne_top — Mathlib

English

An open set U has measure equal to the supremum of the measures of closed subsets contained in U.

Русский

Открытое множество U имеет меру равную максимуму меры замкнутых подмножеств внутри U.

LaTeX

$$$U\text{ open} \Rightarrow μ(U) = \sup\{ μ(F) : F\subseteq U, F\text{ closed} \}$$$

Lean4

/-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
inside by closed sets. -/
theorem _root_.MeasurableSet.exists_lt_isClosed_of_ne_top [WeaklyRegular μ] ⦃A : Set α⦄ (hA : MeasurableSet A)
    (h'A : μ A ≠ ∞) {r : ℝ≥0∞} (hr : r < μ A) : ∃ K, K ⊆ A ∧ IsClosed K ∧ r < μ K :=
  innerRegular_measurable ⟨hA, h'A⟩ _ hr

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