English
Under ContentRegular, for each compact K there exists a K' with K ⊆ interior K' and μ(K') ≤ μ(K) + ε.
Русский
При ContentRegular существует K' с K ⊆ interior(K'), μ(K') ≤ μ(K) + ε.
LaTeX
$$$$\\forall K, ε>0, \\exists K' : \\mathrm{Compacts}(G), K \\subseteq \\operatorname{int}(K') \\land μ(K') \\le μ(K) + ε.$$$$
Lean4
theorem contentRegular_exists_compact (H : ContentRegular μ) (K : TopologicalSpace.Compacts G) {ε : NNReal}
(hε : ε ≠ 0) : ∃ K' : TopologicalSpace.Compacts G, K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ε :=
by
by_contra hc
simp only [not_exists, not_and, not_le] at hc
have lower_bound_iInf :
μ K + ε ≤ ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)
rw [← H] at lower_bound_iInf
exact
(lt_self_iff_false (μ K)).mp
(lt_of_le_of_lt' lower_bound_iInf (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))
