English
There exists a smooth δ: M→ℝ≥0 so that closed balls around x lie inside the open neighborhoods U_i for all i with x in K_i.
Русский
Существует гладкая функция δ, такая что замкнутые шары вокруг x принадлежат соответствующим множествам U_i для всех i с x∈K_i.
LaTeX
$$$\\exists δ ∈ C^∞(I,M;ℝ) : ∀ x, 0<δ(x) ∧ ∀ i, x∈K_i ⇒ EMetric.closedBall(x, δ(x)) ⊆ U_i$$$
Lean4
/-- Let `M` be a smooth σ-compact manifold with extended distance. Let `K : ι → Set M` be a locally
finite family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for
all `i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and
`x ∈ K i`, we have `EMetric.closedBall x (δ x) ⊆ U i`. -/
theorem exists_smooth_forall_closedBall_subset {M} [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
[SigmaCompactSpace M] {K : ι → Set M} {U : ι → Set M} (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i))
(hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
∃ δ : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯, (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i :=
by
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι M] using
exists_smooth_forall_mem_convex_of_local_const I EMetric.exists_forall_closedBall_subset_aux₂
(EMetric.exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)
