instIsCountablyGeneratedAtBotProd

English

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

Русский

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

LaTeX

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

Lean4

instance instIsCountablyGeneratedAtBotProd [Preorder α] [IsCountablyGenerated (atBot : Filter α)] [Preorder β]
    [IsCountablyGenerated (atBot : Filter β)] : IsCountablyGenerated (atBot : Filter (α × β)) :=
  by
  rw [← prod_atBot_atBot_eq]
  infer_instance

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