English
If A has finite μ.outerMeasure, then for every ε > 0 there exists an open set U ⊇ A with μ.outerMeasure(U) ≤ μ.outerMeasure(A) + ε.
Русский
Если μ.outerMeasure(A) конечна, то для любого ε > 0 существует открытое множество U, содержащее A, такое что μ.outerMeasure(U) ≤ μ.outerMeasure(A) + ε.
LaTeX
$$$$\\forall A \\subset G, μ.outerMeasure(A) \\neq \\infty \\Rightarrow \\forall ε \\in \\mathbb{R}_{>0}, \\exists U \\in \\mathrm{Opens}(G), A \\subseteq U \\land μ.outerMeasure(U) \\le μ.outerMeasure(A) + ε.$$$$
Lean4
theorem outerMeasure_exists_open {A : Set G} (hA : μ.outerMeasure A ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0) :
∃ U : Opens G, A ⊆ U ∧ μ.outerMeasure U ≤ μ.outerMeasure A + ε :=
by
rcases
inducedOuterMeasure_exists_set _ μ.innerContent_iUnion_nat μ.innerContent_mono hA (ENNReal.coe_ne_zero.2 hε) with
⟨U, hU, h2U, h3U⟩
exact ⟨⟨U, hU⟩, h2U, h3U⟩
