English
Let X be an extended metric space and K, U families of closed/open sets with inclusions K_i ⊆ U_i and local finiteness. Then there exists a positive continuous function δ: X → ℝ such that for every i and every x ∈ K_i, the closed ball centered at x with radius δ(x) is contained in U_i.
Русский
Пусть X — расширенное метрическое пространство, семейства замкнутых множеств K_i и открытых U_i удовлетворяют условиям K_i ⊆ U_i и локально конечны. Тогда существует положительная непрерывная функция δ: X → ℝ, такая что для каждого i и каждого x ∈ K_i область закрытого шара B̅(x, δ(x)) ⊆ U_i.
LaTeX
$$$\\exists δ: C(X, \\mathbb{R}), (∀ 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, ℝ)` such that for any `i` and `x ∈ K i`,
we have `EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i`. -/
theorem exists_continuous_real_forall_closedBall_subset (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i))
(hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
∃ δ : C(X, ℝ), (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, closedBall x (ENNReal.ofReal <| δ x) ⊆ U i := by
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι X] using
exists_continuous_forall_mem_convex_of_local_const exists_forall_closedBall_subset_aux₂
(exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)
