α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ ε_1, ε_1 > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε_1 → a ⊆ closedBall x ε
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ closedBall x ε
simp only [v.eventually_filterAt_iff]
no goals
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ ε_1, ε_1 > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε_1 → a ⊆ closedBall x ε
exact ⟨ε, hε, fun a _ ha' => ha'⟩