exists_isOpen_diff_lt — Mathlib

English

If A is measurable and μ(A) is finite, there exists an open U ⊇ A with μ(U) finite and μ(U \ A) < ε.

Русский

Если A измеримо и μ(A) меньше бесконечности, существует открытое U ⊇ A с конечной μ(U) и μ(U \ A) < ε.

LaTeX

$$$MeasurableSet\exists\_isOpen\_diff\_lt \ (A)\ (μ)\ (hA) (hA') :\; ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < ∞ ∧ μ (U \ A) < ε$$$

Lean4

theorem _root_.MeasurableSet.exists_isOpen_diff_lt [OuterRegular μ] {A : Set α} (hA : MeasurableSet A) (hA' : μ A ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < ∞ ∧ μ (U \ A) < ε :=
  by
  rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩
  use U, hAU, hUo, hU.trans_le le_top
  exact measure_diff_lt_of_lt_add hA.nullMeasurableSet hAU hA' hU

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