atBot_isCountablyGenerated_of_archimedean

English

Similarly, the atBot filter is countably generated in Archimedean settings.

Русский

Аналогично, фильтр atBot счетно порождается в условиях Архимедовой теории.

LaTeX

$$$\mathrm{atBot}.\mathrm{IsCountablyGenerated}$$$

Lean4

instance (priority := 100) atBot_isCountablyGenerated_of_archimedean [Ring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] : (atBot : Filter R).IsCountablyGenerated :=
  atBot_hasCountableBasis_of_archimedean.isCountablyGenerated

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