α : Type u_2
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
ι : Type u_1
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
α : Type u_2
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
ι : Type u_1
l : Filter ι
f : ι → Set α
x : α
⊢ Tendsto f l (filterAt v x) ↔
    (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
refine' ⟨fun H => ⟨H.eventually <| v.eventually_filterAt_mem_sets x,
  fun ε hε => H.eventually <| v.eventually_filterAt_subset_closedBall x hε⟩,
  fun H s hs => (_ : ∀ᶠ i in l, f i ∈ s)⟩
case intro.intro
α : Type u_2
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
ι : Type u_1
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
α : Type u_2
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
ι : Type u_1
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
obtain ⟨ε, εpos, hε⟩ := v.mem_filterAt_iff.mp hs
no goals
case intro.intro
α : Type u_2
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
ι : Type u_1
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
filter_upwards [H.1, H.2 ε εpos]with i hi hiε using hε _ hi hiε