one_neBot

Mathlib.Order.Filter.Pointwise

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

English

The unit filter is non-bottom: (1 : Filter α).NeBot.

Русский

Единичный фильтр не нижний: (1 : Filter α).NeBot.

LaTeX

$$$(1 : Filter \\alpha).NeBot$$$

Lean4

@[to_additive]
theorem one_neBot : (1 : Filter α).NeBot :=
  Filter.pure_neBot

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

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

Разделы

Аффилиация

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