empty_notMem

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

The empty set never belongs to an ultrafilter.

Русский

Пустое множество никогда не принадлежит ульрафильтру.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)}, \\\\emptyset \\\\notin f$$$

Lean4

@[simp]
theorem empty_notMem : ∅ ∉ f :=
  Filter.empty_notMem (f : Filter α)

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

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

Разделы

Аффилиация

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