pure_neBot

Mathlib.Order.Filter.Map

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

English

For any a, the pure filter at a is NeBot: NeBot (pure a).

Русский

Для любого a чистый фильтр в a является неботовским: NeBot (pure a).

LaTeX

$$$ \mathrm{NeBot} (\mathrm{pure} \ a) $$$

Lean4

instance pure_neBot {α : Type u} {a : α} : NeBot (pure a) :=
  ⟨mt empty_mem_iff_bot.2 <| notMem_empty a⟩

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

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

Разделы

Аффилиация

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