α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
⊢ FineSubfamilyOn v f s
intro x hx ε εpos
case intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
av : a ∈ setsAt v x
ha : a ⊆ closedBall x ε
af : a ∈ f x
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
obtain ⟨a, av, ha, af⟩ : ∃ (a : Set α) , a ∈ v.setsAt x ∧ a ⊆ closedBall x ε ∧ a ∈ f x :=
  v.frequently_filterAt_iff.1 (h x hx) ε εpos
no goals
case intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
av : a ∈ setsAt v x
ha : a ⊆ closedBall x ε
af : a ∈ f x
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
exact ⟨a, ⟨av, af⟩, ha⟩