case intro.intro
ι : Type u_2
X : Type u_1
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
ι : Type u_2
X : Type u_1
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
rcases EMetric.exists_continuous_nNReal_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
case intro.intro
ι : Type u_2
X : Type u_1
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
case intro.intro
ι : Type u_2
X : Type u_1
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
refine' ⟨δ, hδ0, fun i x hx => _⟩
case intro.intro
ι : Type u_2
X : Type u_1
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
case intro.intro
ι : Type u_2
X : Type u_1
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
rw [← emetric_closedBall_nnreal]
no goals
case intro.intro
ι : Type u_2
X : Type u_1
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
exact hδ i x hx