neBot

Mathlib.Order.Filter.Ultrafilter.Defs

URI: https://scilib.ai/kg/mathlib#Ultrafilter.neBot

English

For every ultrafilter f, the underlying filter is nontrivial (NeBot).

Русский

Для каждого ультрафильтра f соответствующий фильтр не тривиален (NeBot).

LaTeX

$$$\forall f:\mathrm{Ultrafilter}(\alpha),\; (f:\mathrm{Filter}(\alpha)).\mathrm{NeBot}$$$

Lean4

instance neBot (f : Ultrafilter α) : NeBot (f : Filter α) :=
  f.neBot'

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

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

Разделы

Аффилиация

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