univ_mem

Mathlib.Order.Filter.Defs

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

English

The universal set is always a member of any filter.

Русский

Единица вселенного множества (univ) всегда принадлежит любому фильтру.

LaTeX

$$$\forall f:\text{Filter}(\alpha),\ univ\in f$$$

Lean4

@[simp]
theorem univ_mem : univ ∈ f :=
  f.univ_sets

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

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

Разделы

Аффилиация

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