isCountablyGenerated

Mathlib.Order.Filter.AtTopBot.CountablyGenerated

URI: https://scilib.ai/kg/mathlib#Filter.atBot.isCountablyGenerated

← MathLib Explorer

English

The filter atBot on α is countably generated (under standard hypotheses).

Русский

Фильтр atBot на α счётно порождён.

LaTeX

$$$$\operatorname{IsCountablyGenerated}(\operatorname{atBot}_{\alpha}).$$$$

Lean4

instance (priority := 200) isCountablyGenerated [Preorder α] [Countable α] :
    (atBot : Filter <| α).IsCountablyGenerated :=
  isCountablyGenerated_seq _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru