α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ s ∈ map (fun r => closedBall x r) (𝓝[Ioi 0] 0)
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
⊢ Tendsto (fun r => closedBall x r) (𝓝[Ioi 0] 0) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x)
intro s hs
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ s ∈ map (fun r => closedBall x r) (𝓝[Ioi 0] 0)
simp only [mem_map]
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
obtain ⟨ε, εpos, hε⟩ :
  ∃ (ε : ℝ), ε > 0 ∧
    ∀ a : Set α, a ∈ (Besicovitch.vitaliFamily μ).setsAt x → a ⊆ closedBall x ε → a ∈ s :=
  (VitaliFamily.mem_filterAt_iff _).1 hs
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
have : Ioc (0 : ℝ) ε ∈ 𝓝[>] (0 : ℝ) := Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, εpos⟩
case h
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ a✝ ∈ (fun r => closedBall x r) ⁻¹' s
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
⊢ (fun r => closedBall x r) ⁻¹' s ∈ 𝓝[Ioi 0] 0
filter_upwards [this] with _ hr
case h.a
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ (fun r => closedBall x r) a✝ ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x

case h.a
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ (fun r => closedBall x r) a✝ ⊆ closedBall x ε
case h
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ a✝ ∈ (fun r => closedBall x r) ⁻¹' s
apply hε
no goals
case h.a
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ (fun r => closedBall x r) a✝ ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x
exact mem_image_of_mem _ hr.1
no goals
case h.a
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x → a ⊆ closedBall x ε → a ∈ s
this : Ioc 0 ε ∈ 𝓝[Ioi 0] 0
a✝ : ℝ
hr : a✝ ∈ Ioc 0 ε
⊢ (fun r => closedBall x r) a✝ ⊆ closedBall x ε
exact closedBall_subset_closedBall hr.2