English
Let X be an extended metric space, K_i closed, U_i open with K_i ⊆ U_i and locally finite. Then there exists a positive continuous δ: 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, локально конечны. Тогда существует положительная непрерывная δ: X → ℝ≥0∞ такая, что для каждого i и x ∈ K_i выполнено closedBall x (δ(x)) ⊆ U_i.
LaTeX
$$$\\exists δ: C(X, \\mathbb{R}_{\\ge 0\\!\\!\\infty}), (∀ 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_eNNReal_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 :=
let ⟨δ, hδ₀, hδ⟩ := exists_continuous_nnreal_forall_closedBall_subset hK hU hKU hfin
⟨ContinuousMap.comp ⟨Coe.coe, ENNReal.continuous_coe⟩ δ, fun x => ENNReal.coe_pos.2 (hδ₀ x), hδ⟩
