sigma — Mathlib

English

A disjoint union (sigma-type) of completely metrizable spaces is completely metrizable.

Русский

Расщепление по индексу двух полностью метризуемых пространств сохраняет метризуемость.

LaTeX

$$$\\forall ι\\, {X : ι \\to Type*},\\ [\\forall n, TopologicalSpace (X n)], [\\forall n, IsCompletelyMetrizableSpace (X n)]\\Rightarrow IsCompletelyMetrizableSpace (\\Sigma n, X n)$$$

Lean4

/-- A disjoint union of completely metrizable spaces is completely metrizable. -/
instance sigma {ι : Type*} {X : ι → Type*} [∀ n, TopologicalSpace (X n)] [∀ n, IsCompletelyMetrizableSpace (X n)] :
    IsCompletelyMetrizableSpace (Σ n, X n) :=
  letI := fun n ↦ upgradeIsCompletelyMetrizable (X n)
  letI : MetricSpace (Σ n, X n) := Metric.Sigma.metricSpace
  haveI : CompleteSpace (Σ n, X n) := Metric.Sigma.completeSpace
  inferInstance

Похожие утверждения