nonempty_of_neBot

Mathlib.Order.Filter.Basic

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

English

If f is a NeBot filter on α, then α is nonempty.

Русский

Если f — неботовый фильтр на α, то α непусто.

LaTeX

$$$\operatorname{Nonempty}(\alpha)$$$

Lean4

theorem nonempty_of_neBot (f : Filter α) [NeBot f] : Nonempty α :=
  Exists.nonempty <| nonempty_of_mem (univ_mem : univ ∈ f)

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

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

Разделы

Аффилиация

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