atTop_neBot

Mathlib.Order.Filter.AtTopBot.Basic

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

English

The atTop filter is nontrivial (NeBot) whenever the index set is nonempty and directed.

Русский

Фильтр atTop является ненулевым (NeBot), когда множество индексов непусто и направлено.

LaTeX

$$$ \\operatorname{atTop}.\\mathrm{NeBot}$$$

Lean4

@[instance]
theorem atTop_neBot : NeBot (atTop : Filter α) :=
  atTop_basis.neBot_iff.2 fun _ => nonempty_Ici

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

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

Разделы

Аффилиация

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