English
In a complete metric space, any nonempty perfect set C can be split into two disjoint nonempty perfect subsets C0 and C1 contained in C, each with diameter at most ε, for any ε>0.
Русский
В полной метрической пространстве любую непустую совершенную подмножественную фигуру C можно разложить на две непересекающиеся непустые совершенные подмножества C0 и C1, лежащие в C и имеющие диаметр не более ε.
LaTeX
$$$\\exists C_0, C_1 \\subseteq \\alpha,\\ (Perfect C_0 ∧ C_0 \\neq ∅ ∧ C_0 ⊆ C ∧ diam(C_0) ≤ ε) ∧ (Perfect C_1 ∧ C_1 \\neq ∅ ∧ C_1 ⊆ C ∧ diam(C_1) ≤ ε) ∧ Disjoint(C_0, C_1)$$$
Lean4
/-- A refinement of `Perfect.splitting` for metric spaces, where we also control
the diameter of the new perfect sets. -/
theorem small_diam_splitting (hC : Perfect C) (hnonempty : C.Nonempty) (ε_pos : 0 < ε) :
∃ C₀ C₁ : Set α,
(Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
(Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁ :=
by
rcases hC.splitting hnonempty with ⟨D₀, D₁, ⟨perf0, non0, sub0⟩, ⟨perf1, non1, sub1⟩, hdisj⟩
obtain ⟨x₀, hx₀⟩ := non0
obtain ⟨x₁, hx₁⟩ := non1
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩
rcases perf1.small_diam_aux ε_pos hx₁ with ⟨perf1', non1', sub1', diam1⟩
refine
⟨closure (EMetric.ball x₀ (ε / 2) ∩ D₀), closure (EMetric.ball x₁ (ε / 2) ∩ D₁),
⟨perf0', non0', sub0'.trans sub0, diam0⟩, ⟨perf1', non1', sub1'.trans sub1, diam1⟩, ?_⟩
apply Disjoint.mono _ _ hdisj <;> assumption
