pi_countable — Mathlib

English

A countable product of completely metrizable spaces is completely metrizable.

Русский

Счётное произведение полностью метризуемых пространств является полностью метризуемым.

LaTeX

$$$\\forall ι\\, [Countable ι],\\forall X:\\ ι\\to Type*,\\(\\forall i, TopologicalSpace (X i))\\ (\\forall i, IsCompletelyMetrizableSpace (X i))\\Rightarrow IsCompletelyMetrizableSpace (\\prod i, X i)$$$

Lean4

/-- A countable product of completely metrizable spaces is completely metrizable. -/
instance pi_countable {ι : Type*} [Countable ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, IsCompletelyMetrizableSpace (X i)] : IsCompletelyMetrizableSpace (Π i, X i) :=
  by
  letI := fun i ↦ upgradeIsCompletelyMetrizable (X i)
  infer_instance

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