English
Let X be a metric space, with locally finite closed K_i and open U_i containing K_i. There exists a positive continuous δ: X → ℝ such that for all i and x ∈ K_i, closedBall x (δ(x)) ⊆ U_i.
Русский
Пусть X — метрическое пространство, K_i локально конечны и замкнуты, U_i открыты и содержат K_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 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, ℝ)` such that for any `i` and `x ∈ K i`, we have
`Metric.closedBall x (δ 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 (δ x) ⊆ U i :=
let ⟨δ, hδ₀, hδ⟩ := exists_continuous_nnreal_forall_closedBall_subset hK hU hKU hfin
⟨ContinuousMap.comp ⟨Coe.coe, NNReal.continuous_coe⟩ δ, hδ₀, hδ⟩
