English
In a separable space, for any ε>0 there exists a countable partition by measurable bounded-diameter sets that covers the space and is pairwise disjoint.
Русский
В разделимом пространстве существует счётное разбиение на измеримые множества шаров диаметром ≤ ε, покрывающее всё пространство и попарно попарное непересечение.
LaTeX
$$$\\exists (A_n)_{n\\in\\mathbb{N}} ,\\; \\forall n, \\text{Measurable}(A_n) \\land \\operatorname{diam}(A_n) ≤ ε \\land \\bigcup_n A_n = \\Omega \\land \\text{Pairwise Disjoint}(A_n).$$$
Lean4
/-- In a separable pseudometric space, for any ε > 0 there exists a countable collection of
disjoint Borel measurable subsets of diameter at most ε that cover the whole space. -/
theorem exists_measurable_partition_diam_le {ε : ℝ} (ε_pos : 0 < ε) :
∃ (As : ℕ → Set Ω),
(∀ n, MeasurableSet (As n)) ∧
(∀ n, Bornology.IsBounded (As n)) ∧
(∀ n, diam (As n) ≤ ε) ∧ (⋃ n, As n = univ) ∧ (Pairwise (fun (n m : ℕ) ↦ Disjoint (As n) (As m))) :=
by
cases isEmpty_or_nonempty Ω
· refine
⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_, fun _ _ _ ↦
disjoint_of_subsingleton⟩
· intro n
simpa only [diam_empty] using ε_pos.le
· subsingleton
obtain ⟨xs, xs_dense⟩ := exists_dense_seq Ω
have half_ε_pos : 0 < ε / 2 := half_pos ε_pos
set Bs := fun n ↦ Metric.ball (xs n) (ε / 2)
set As := disjointed Bs
refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
· exact MeasurableSet.disjointed (fun n ↦ measurableSet_ball)
· exact fun n ↦ Bornology.IsBounded.subset isBounded_ball <| disjointed_subset Bs n
· intro n
apply (diam_mono (disjointed_subset Bs n) isBounded_ball).trans
convert diam_ball half_ε_pos.le
ring
· have aux : ⋃ n, Bs n = univ :=
by
convert DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos
exact (ball_eq_ball' _ _).symm
simpa only [← aux] using iUnion_disjointed
· exact disjoint_disjointed Bs
