English
A disjoint union of complete metric spaces is complete.
Русский
Дизъюнктивное объединение непустых полных метрических пространств полно.
LaTeX
$$$\text{If } \forall i,\; E_i\text{ is complete, then } \Sigma_i E_i\text{ is complete.}$$$
Lean4
/-- A disjoint union of complete metric spaces is complete. -/
protected theorem completeSpace [∀ i, CompleteSpace (E i)] : CompleteSpace (Σ i, E i) :=
by
set s : ι → Set (Σ i, E i) := fun i => Sigma.fst ⁻¹' { i }
set U := {p : (Σ k, E k) × Σ k, E k | dist p.1 p.2 < 1}
have hc : ∀ i, IsComplete (s i) := fun i =>
by
simp only [s, ← range_sigmaMk]
exact (isometry_mk i).isUniformInducing.isComplete_range
have hd : ∀ (i j), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j := fun i j x hx y hy hxy =>
(Eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy)
refine completeSpace_of_isComplete_univ ?_
convert isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd
simp only [s, ← preimage_iUnion, iUnion_of_singleton, preimage_univ]
