univ_mem'

Mathlib.Order.Filter.Defs

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

English

If s contains every element, then s is in any filter.

Русский

Если множество содержит каждый элемент, то оно принадлежит любому фильтру.

LaTeX

$$$\forall f:\text{Filter}(\alpha),\forall s:\Set\alpha, (\forall a:\alpha, a\in s) \Rightarrow s\in f$$$

Lean4

theorem univ_mem' (h : ∀ a, a ∈ s) : s ∈ f :=
  mem_of_superset univ_mem fun x _ => h x

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

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

Разделы

Аффилиация

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