isCountablyGenerated_bot

Mathlib.Order.Filter.CountablyGenerated

URI: https://scilib.ai/kg/mathlib#Filter.isCountablyGenerated_bot

English

IsCountablyGenerated_bot: IsCountablyGenerated (⊥ : Filter α).

Русский

IsCountablyGenerated_bot: IsCountablyGenerated (⊥ : Filter α).

LaTeX

$$$\\operatorname{IsCountablyGenerated}(\\perp\\, : \\text{Filter }\\alpha)$$$

Lean4

@[instance]
theorem isCountablyGenerated_bot : IsCountablyGenerated (⊥ : Filter α) :=
  @principal_empty α ▸ isCountablyGenerated_principal _

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

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

Разделы

Аффилиация

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