nonempty_of_mem

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

If s ∈ f, then s is nonempty.

Русский

Если s ∈ f, то s не пусто.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {s \\\\subseteq \\\\alpha}, s \\\\in f \\\\Rightarrow s.\\\\Nonempty$$$

Lean4

theorem nonempty_of_mem (hs : s ∈ f) : s.Nonempty :=
  Filter.nonempty_of_mem hs

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

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

Разделы

Аффилиация

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