English
If μ is outer regular and μ(A) < r, there exists an open U ⊇ A with μ(U) < r.
Русский
Если μ_outer регулярна и μ(A) < r, существует открытое U, содержащее A, такое что μ(U) < r.
LaTeX
$$$OuterRegular(\mu) \Rightarrow (\forall A, μ(A) < r \Rightarrow \exists U \supseteq A, IsOpen(U) \land μ(U) < r).$$$
Lean4
/-- Given `r` larger than the measure of a set `A`, there exists an open superset of `A` with
measure less than `r`. -/
theorem _root_.Set.exists_isOpen_lt_of_lt [OuterRegular μ] (A : Set α) (r : ℝ≥0∞) (hr : μ A < r) :
∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < r :=
by
rcases OuterRegular.outerRegular (measurableSet_toMeasurable μ A) r (by rwa [measure_toMeasurable]) with
⟨U, hAU, hUo, hU⟩
exact ⟨U, (subset_toMeasurable _ _).trans hAU, hUo, hU⟩
