[GOAL]
ι : Type u_1
X : Type u_2
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
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
  by
  apply
    mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
      (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
  apply univ_mem'
  rintro ⟨r, y⟩ hxy hyU i hi
  simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy 
  exact hyU _ (hxy _ hi)
[GOAL]
ι : Type u_1
X : Type u_2
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 : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
apply
  mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
    (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
[GOAL]
ι : Type u_1
X : Type u_2
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 : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ {x_1 |
      x_1 ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ →
        x_1 ∈
          {x_2 |
            x_2 ∈ {x_3 | (fun x_4 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_4.snd x_4.fst ⊆ U i) x_3} →
              x_2 ∈ {x | (fun p => ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i) x}}} ∈
    𝓝 0 ×ˢ 𝓝 x
[PROOFSTEP]
apply univ_mem'
[GOAL]
case h
ι : Type u_1
X : Type u_2
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 : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ ∀ (a : ℝ≥0∞ × X),
    a ∈
      {x_1 |
        x_1 ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ →
          x_1 ∈
            {x_2 |
              x_2 ∈ {x_3 | (fun x_4 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_4.snd x_4.fst ⊆ U i) x_3} →
                x_2 ∈ {x | (fun p => ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i) x}}}
[PROOFSTEP]
rintro ⟨r, y⟩ hxy hyU i hi
[GOAL]
case h.mk
ι : Type u_1
X : Type u_2
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 : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
r : ℝ≥0∞
y : X
hxy : (r, y) ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_2.snd x_2.fst ⊆ U i) x_1}
i : ι
hi : (r, y).snd ∈ K i
⊢ closedBall (r, y).snd (r, y).fst ⊆ U i
[PROOFSTEP]
simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy 
[GOAL]
case h.mk
ι : Type u_1
X : Type u_2
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 : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
r : ℝ≥0∞
y : X
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_2.snd x_2.fst ⊆ U i) x_1}
i : ι
hi : (r, y).snd ∈ K i
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedBall (r, y).snd (r, y).fst ⊆ U i
[PROOFSTEP]
exact hyU _ (hxy _ hi)
[GOAL]
ι : Type u_1
X : Type u_2
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
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
rcases nhds_basis_closed_eball.mem_iff.1 ((hU i).mem_nhds <| hKU i hi) with ⟨R, hR₀, hR⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_nnreal_btwn.mp hR₀ with ⟨r, hr₀, hrR⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
filter_upwards [prod_mem_prod (eventually_lt_nhds hr₀) (closedBall_mem_nhds x (tsub_pos_iff_lt.2 hrR))] with p hp z hz
[GOAL]
case h
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ z ∈ U i
[PROOFSTEP]
apply hR
[GOAL]
case h.a
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ z ∈ closedBall x R
[PROOFSTEP]
calc
  edist z x ≤ edist z p.2 + edist p.2 x := edist_triangle _ _ _
  _ ≤ p.1 + (R - p.1) := (add_le_add hz <| le_trans hp.2 <| tsub_le_tsub_left hp.1.out.le _)
  _ = R := add_tsub_cancel_of_le (lt_trans (by exact hp.1) hrR).le
[GOAL]
ι : Type u_1
X : Type u_2
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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ p.fst < ↑r
[PROOFSTEP]
exact hp.1
[GOAL]
ι : Type u_1
X : Type u_2
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}
[PROOFSTEP]
have :=
  (ENNReal.continuous_ofReal.tendsto' 0 0 ENNReal.ofReal_zero).eventually
    (eventually_nhds_zero_forall_closedBall_subset hK hU hKU hfin x).curry
[GOAL]
ι : Type u_1
X : Type u_2
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}
[PROOFSTEP]
rcases this.exists_gt with ⟨r, hr0, hr⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
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}
[PROOFSTEP]
refine' ⟨r, hr.mono fun y hy => ⟨hr0, _⟩⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
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}
[PROOFSTEP]
rwa [mem_preimage, mem_iInter₂]
[GOAL]
ι : Type u_1
X : Type u_2
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), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
[PROOFSTEP]
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι X] using
  exists_continuous_forall_mem_convex_of_local_const exists_forall_closedBall_subset_aux₂
    (exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)
[GOAL]
ι : Type u_1
X : Type u_2
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), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rcases exists_continuous_real_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
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
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
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
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < ↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x
hδ :
  ∀ (i : ι) (x : X),
    x ∈ K i → closedBall x (ENNReal.ofReal (↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
refine' ⟨δ, hδ₀, fun i x hi => _⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
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
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < ↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x
hδ :
  ∀ (i : ι) (x : X),
    x ∈ K i → closedBall x (ENNReal.ofReal (↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x)) ⊆ U i
i : ι
x : X
hi : x ∈ K i
⊢ closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace 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), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rcases EMetric.exists_continuous_nNReal_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
refine' ⟨δ, hδ0, fun i x hx => _⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rw [← emetric_closedBall_nnreal]
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ EMetric.closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
exact hδ i x hx
