ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
have := (ENNReal.continuous_ofReal.tendsto' 0 0 ENNReal.ofReal_zero).eventually
  (eventually_nhds_zero_forall_closedBall_subset hK hU hKU hfin x).curry
case intro.intro
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
rcases this.exists_gt with ⟨r, hr0, hr⟩
case intro.intro
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
case intro.intro
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
refine' ⟨r, hr.mono fun y hy => ⟨hr0, _⟩⟩
no goals
case intro.intro
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
rwa [mem_preimage, mem_iInter₂]