English
Let μ be a regular measure. Then every open set can be approximated from inside by compact sets: for every open U and every r with r < μ(U), there exists a compact K ⊆ U such that μ(K) > r.
Русский
Пусть μ — регулярная мера. Тогда любой открытый множество можно аппроксимировать изнутри компактными подмножествами: для каждого открытого множества U и для любого r < μ(U) существует компактное K ⊆ U такое, что μ(K) > r.
LaTeX
$$$\\text{If } \\mu \\text{ is regular, then for every open } U \\text{ and every } r \\text{ with } r < \\mu(U), \\exists K \\subseteq U \\text{ compact with } r < \\mu(K).$$$
Lean4
/-- If `μ` is a regular measure, then any open set can be approximated by a compact subset. -/
theorem _root_.IsOpen.exists_lt_isCompact [Regular μ] ⦃U : Set α⦄ (hU : IsOpen U) {r : ℝ≥0∞} (hr : r < μ U) :
∃ K, K ⊆ U ∧ IsCompact K ∧ r < μ K :=
Regular.innerRegular hU r hr
