English
If U is open and μ.outerMeasure(U) ≠ ∞, then for every ε > 0 there exists a compact K ⊆ U such that μ.outerMeasure(U) ≤ μ.outerMeasure(K) + ε.
Русский
Если U открыто и μ.outerMeasure(U) ≠ ∞, то для любого ε > 0 существует компактное K ⊆ U такое, что μ.outerMeasure(U) ≤ μ.outerMeasure(K) + ε.
LaTeX
$$$$\\forall {U} \\in \\mathrm{Opens}(G), μ.outerMeasure(U) \\neq \\infty \\Rightarrow \\forall ε \\in \\mathbb{R}_{>0}, \\exists K \\in \\mathrm{Compacts}(G), (K \\subseteq U) \\land μ.outerMeasure(U) \\le μ.outerMeasure(K) + ε.$$$$
Lean4
theorem outerMeasure_exists_compact {U : Opens G} (hU : μ.outerMeasure U ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0) :
∃ K : Compacts G, (K : Set G) ⊆ U ∧ μ.outerMeasure U ≤ μ.outerMeasure K + ε :=
by
rw [μ.outerMeasure_opens] at hU ⊢
rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩
exact ⟨K, h1K, le_trans h2K <| add_le_add_right (μ.le_outerMeasure_compacts K) _⟩
