English
If μ.innerContent(U) is finite for an open U and ε > 0, there exists a compact K ⊆ U with μ.innerContent U ≤ μ(K) + ε.
Русский
Если μ.innerContent(U) конечно, то найдется компактное K ⊆ U такое, что μ.innerContent(U) ≤ μ(K) + ε.
LaTeX
$$$μ.innerContent U ≠ ∞ \Rightarrow \exists K \; (K \subseteq U) ∧ μ.innerContent U ≤ μ(K) + ε$$$
Lean4
theorem innerContent_exists_compact {U : Opens G} (hU : μ.innerContent U ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0) :
∃ K : Compacts G, (K : Set G) ⊆ U ∧ μ.innerContent U ≤ μ K + ε :=
by
have h'ε := ENNReal.coe_ne_zero.2 hε
rcases le_or_gt (μ.innerContent U) ε with h | h
· exact ⟨⊥, empty_subset _, le_add_left h⟩
have h₂ := ENNReal.sub_lt_self hU h.ne_bot h'ε
conv at h₂ => rhs; rw [innerContent]
simp only [lt_iSup_iff] at h₂
rcases h₂ with ⟨U, h1U, h2U⟩; refine ⟨U, h1U, ?_⟩
rw [← tsub_le_iff_right]; exact le_of_lt h2U
