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
δ : 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
ι : 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), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
rcases exists_continuous_real_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩
case intro.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
δ : 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
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
δ : 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
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le
case intro.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
δ : 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
case intro.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
δ : 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
refine' ⟨δ, hδ₀, fun i x hi => _⟩
no goals
case intro.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
δ : 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
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi