instSecondCountableTopologyProd — Mathlib

English

The product of two second-countable spaces is second-countable.

Русский

Произведение двух пространств с двойной счетностью также имеет двойную счетность.

LaTeX

$$$[SecondCountableTopology(\alpha)] \land [SecondCountableTopology(\beta)] \Rightarrow SecondCountableTopology(\alpha \times \beta)$$$

Lean4

instance {β : Type*} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] :
    SecondCountableTopology (α × β) :=
  ((isBasis_countableBasis α).prod (isBasis_countableBasis β)).secondCountableTopology <|
    (countable_countableBasis α).image2 (countable_countableBasis β) _

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