English
The disjoint sigma-sum of completely metrizable spaces is completely metrizable.
Русский
Расщепление по индексу двух полностью метризуемых пространств сохраняет метризуемость.
LaTeX
$$$\\forall ι\\, {X : ι \\to Type*}\\ [\\forall n, TopologicalSpace (X n)][\\forall n, IsCompletelyMetrizableSpace (X n)]\\Rightarrow IsCompletelyMetrizableSpace (Σ n, X n)$$$
Lean4
/-- The maximal pseudo metric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
where `d : X → X → ℝ≥0` is a function such that `d x x = 0` and `d x y = d y x` for all `x`, `y`. -/
noncomputable def ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0) (dist_comm : ∀ x y, d x y = d y x) :
PseudoMetricSpace X
where
dist x y := ↑(⨅ l : List X, ((x :: l).zipWith d (l ++ [y])).sum : ℝ≥0)
dist_self
x :=
NNReal.coe_eq_zero.2 <| nonpos_iff_eq_zero.1 <| (ciInf_le (OrderBot.bddBelow _) []).trans_eq <| by simp [dist_self]
dist_comm x
y :=
NNReal.coe_inj.2 <| by
refine reverse_surjective.iInf_congr _ fun l ↦ ?_
rw [← sum_reverse, reverse_zipWith, reverse_append, reverse_reverse, reverse_singleton, singleton_append,
reverse_cons, reverse_reverse, zipWith_comm_of_comm dist_comm]
simp only [length, length_append]
dist_triangle x y
z := by
rw [← NNReal.coe_add, NNReal.coe_le_coe]
refine NNReal.le_iInf_add_iInf fun lxy lyz ↦ ?_
calc
⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤ (zipWith d (x :: lxy ++ y :: lyz) ((lxy ++ y :: lyz) ++ [z])).sum :=
ciInf_le (OrderBot.bddBelow _) (lxy ++ y :: lyz)
_ = (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum :=
by
rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc, append_assoc,
append_assoc]
rw [length_cons, length_append, length_singleton]
