instCountablyGeneratedProd — Mathlib

English

If α and β are countably generated, then α × β is countably generated.

Русский

Если пространства α и β счётно порождаются, то их произведение α × β тоже порождается.

LaTeX

$$$ \text{CountablyGenerated}(\alpha \times \beta) $$$

Lean4

instance [MeasurableSpace α] [CountablyGenerated α] [MeasurableSpace β] [CountablyGenerated β] :
    CountablyGenerated (α × β) :=
  .sup (.comap Prod.fst) (.comap Prod.snd)

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