English
Let X be a metric space and K_i closed, U_i open with K_i ⊆ U_i, and {K_i} locally finite. Then there exists δ ∈ C(X, ℝ≥0) with δ(x) > 0 such that for all i and x ∈ K_i, closedBall x (δ(x)) ⊆ U_i.
Русский
Пусть X — метрическое пространство, K_i замкнуты, U_i открыты и K_i ⊆ U_i, локально конечны. Тогда существует δ ∈ C(X, ℝ≥0) с δ(x)>0, такая что для всех i и x ∈ K_i выполнено closedBall x (δ(x)) ⊆ U_i.
LaTeX
$$$\\exists δ: C(X, \\mathbb{R}_{\\ge 0}), (∀ x, 0 < δ(x)) ∧ ∀ i, ∀ x ∈ K_i, closedBall x (δ(x)) ⊆ U_i$$$
Lean4
/-- Let `X` be a metric space. Let `K : ι → Set X` be a locally finite family of closed sets, let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a
positive continuous function `δ : C(X, ℝ≥0)` such that for any `i` and `x ∈ K i`, we have
`Metric.closedBall x (δ x) ⊆ U i`. -/
theorem exists_continuous_nnreal_forall_closedBall_subset (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i))
(hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
∃ δ : C(X, ℝ≥0), (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i :=
by
rcases EMetric.exists_continuous_nnreal_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
refine ⟨δ, hδ0, fun i x hx => ?_⟩
rw [← emetric_closedBall_nnreal]
exact hδ i x hx
