α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ o
rw [eventually_filterAt_iff]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ o
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
rcases Metric.mem_nhds_iff.1 hx with ⟨ε, εpos, hε⟩
no goals
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ o
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
exact ⟨ε / 2, half_pos εpos,
  fun a _ ha => ha.trans ((closedBall_subset_ball (half_lt_self εpos)).trans hε)⟩