English
Given a measurable set s of finite measure, one can approximate s in measure by an open set U, controlling the symmetric difference μ(U Δ s).
Русский
Для измеряемого множества s конечного меры можно аппроксимировать s по мере открытым множеством U, контролируя меру симметрического различия μ(U Δ s).
LaTeX
$$$s\text{ measurable},\ μ(s) < ∞\Rightarrow ∃ U(\text{open}):\ μ(U\Delta s) < ε$$$
Lean4
instance smul [h : InnerRegularCompactLTTop μ] (c : ℝ≥0∞) : InnerRegularCompactLTTop (c • μ) :=
by
by_cases hc : c = 0
· simp only [hc, zero_smul]
infer_instance
by_cases h'c : c = ∞
· constructor
intro s hs r hr
by_cases h's : μ s = 0
· simp [h's] at hr
· simp [h'c, h's] at hs
· constructor
convert InnerRegularWRT.smul h.innerRegular c using 2 with s
have : (c • μ) s ≠ ∞ ↔ μ s ≠ ∞ := by simp [ENNReal.mul_eq_top, hc, h'c]
simp only [this]
