instIsCountablyGeneratedAtTop — Mathlib

English

In the order dual, if atBot is countably generated, then atTop in the dual order is countably generated.

Русский

В порядке двойственности, если atBot счётно порожден, то atTop в двойственном порядке счётно порожден.

LaTeX

$$$$\operatorname{IsCountablyGenerated}(\operatorname{atTop}_{\alpha^{\mathrm{op}}}).$$$$

Lean4

instance _root_.OrderDual.instIsCountablyGeneratedAtTop [Preorder α] [IsCountablyGenerated (atBot : Filter α)] :
    IsCountablyGenerated (atTop : Filter αᵒᵈ) :=
  ‹_›

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