isCountablyGenerated_top

Mathlib.Order.Filter.CountablyGenerated

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

English

IsCountablyGenerated_top: IsCountablyGenerated (⊤ : Filter α).

Русский

IsCountablyGenerated_top: IsCountablyGenerated (⊤ : Filter α).

LaTeX

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

Lean4

@[instance]
theorem isCountablyGenerated_top : IsCountablyGenerated (⊤ : Filter α) :=
  @principal_univ α ▸ isCountablyGenerated_principal _

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

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

Разделы

Аффилиация

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