instIsCountablyGeneratedAtTopProd

English

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

Русский

Если atTop на α и atTop на β счётно порождены, то atTop на α × β счётно порождён.

LaTeX

$$$$\operatorname{IsCountablyGenerated}(\operatorname{atTop}_{\alpha}) \land \operatorname{IsCountablyGenerated}(\operatorname{atTop}_{\beta}) \Rightarrow \operatorname{IsCountablyGenerated}(\operatorname{atTop}_{\alpha\times\beta}).$$$$

Lean4

instance instIsCountablyGeneratedAtTopProd [Preorder α] [IsCountablyGenerated (atTop : Filter α)] [Preorder β]
    [IsCountablyGenerated (atTop : Filter β)] : IsCountablyGenerated (atTop : Filter (α × β)) :=
  by
  rw [← prod_atTop_atTop_eq]
  infer_instance

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