atTop_eq_generate_Ici

Mathlib.Order.Filter.AtTopBot.Defs

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

English

The filter atTop is generated by the family of upward rays Ici a as a runs through α.

Русский

Фильтр atTop порождается семейством множеств Ici a по всем a ∈ α.

LaTeX

$$$\\mathrm{atTop} = \\mathrm{generate}(\\mathrm{range}(\\mathrm{Ici})).$$$

Lean4

theorem atTop_eq_generate_Ici [Preorder α] : atTop = generate (range (Ici (α := α))) := by
  simp only [generate_eq_biInf, atTop, iInf_range]

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

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

Разделы

Аффилиация

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