case intro.intro.intro
α : Type u_1
β : Type ?u.13200
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
hA : MeasurableSet A
hA' : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < ⊤ ∧ ↑↑μ (U \ A) < ε
α : Type u_1
β : Type ?u.13200
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
hA : MeasurableSet A
hA' : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < ⊤ ∧ ↑↑μ (U \ A) < ε
rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.13200
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
hA : MeasurableSet A
hA' : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ↑↑μ (U \ A) < ε
case intro.intro.intro
α : Type u_1
β : Type ?u.13200
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
hA : MeasurableSet A
hA' : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < ⊤ ∧ ↑↑μ (U \ A) < ε
use U, hAU, hUo, hU.trans_le le_top
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.13200
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
hA : MeasurableSet A
hA' : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ↑↑μ (U \ A) < ε
exact measure_diff_lt_of_lt_add hA hAU hA' hU