instSecondCountableTopologyForallOfCountable

English

A countable index family of spaces each second-countable yields a second-countable product space.

Русский

Счетное множество индексов пространств, каждое из которых вторично счетно, даёт вторично счетное произведение.

LaTeX

$$$\exists\; \text{Countable } ι,\; \forall a, SecondCountableTopology(X(a)) \Rightarrow SecondCountableTopology(\forall a, X(a))$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (X a)] [∀ a, SecondCountableTopology (X a)] :
    SecondCountableTopology (∀ a, X a) :=
  secondCountableTopology_iInf fun _ =>
    secondCountableTopology_induced _ _
      _
        -- see Note [lower instance priority]

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