English
Let X be an extended metric space with locally finite closed K_i and open U_i with K_i ⊆ U_i. Then there exists a positive continuous δ: X → ℝ≥0 such that for every i and x ∈ K_i, closedBall x (δ(x)) ⊆ U_i.
Русский
Пусть X — расширенное метрическое пространство, локально конечная семья замкнутых K_i и открытых U_i с K_i ⊆ U_i. Тогда существует положительная непрерывная δ: 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 an extended 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 `EMetric.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 exists_continuous_real_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le
refine ⟨δ, hδ₀, fun i x hi => ?_⟩
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi
