English
Let R be a positive function on a proper metric space; there exists a collection of balls with radii r_i, r'_i such that r_i < r'_i < R(c_i), and the family of balls {ball(c_i, r'_i)} is locally finite, while {ball(c_i, r_i)} covers the space.
Русский
Пусть есть положительная функция R на корректном метрическом пространстве; существует коллекция шаров с радиусами r_i < r'_i < R(c_i), такая что {ball(c_i, r'_i)} локально конечно, а {ball(c_i, r_i)} покрывает пространство.
LaTeX
$$$\\exists \\iota \\to \\alpha, c, r, r' \\text{ с } 0 < r_i < r'_i < R(c_i),\\ LocallyFinite(\\{ball(c_i, r'_i)\\})\\text{ и } X = \\bigcup_i ball(c_i, r_i).$$$
Lean4
/-- Let `R : α → ℝ` be a (possibly discontinuous) positive function on a proper metric space. Then
there exists a collection of pairs of balls `Metric.ball (c i) (r i)`, `Metric.ball (c i) (r' i)`
such that
* for all `i` we have `0 < r i < r' i < R (c i)`;
* the family of balls `Metric.ball (c i) (r' i)` is locally finite;
* the balls `Metric.ball (c i) (r i)` cover the whole space.
This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`
and `exists_iUnion_ball_eq_radius_pos_lt` or `exists_locallyFinite_subset_iUnion_ball_radius_lt`. -/
theorem exists_locallyFinite_iUnion_eq_ball_radius_lt {R : α → ℝ} (hR : ∀ x, 0 < R x) :
∃ (ι : Type u) (c : ι → α) (r r' : ι → ℝ),
(∀ i, 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
(LocallyFinite fun i => ball (c i) (r' i)) ∧ ⋃ i, ball (c i) (r i) = univ :=
let ⟨ι, c, r, r', hlt, hfin, hsub⟩ := exists_locallyFinite_subset_iUnion_ball_radius_lt isClosed_univ fun x _ => hR x
⟨ι, c, r, r', fun i => (hlt i).2, hfin, univ_subset_iff.1 hsub⟩
