mem_top_iff_forall

Mathlib.Order.Filter.Defs

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

English

A set s is in the top filter iff it contains every element of α.

Русский

Множество s принадлежит верхнему фильтру тогда и только тогда, когда оно содержит каждый элемент α.

LaTeX

$$$s \\in (\\top : Filter \\alpha) \\iff \\forall x : \\alpha, x \\in s$$$

Lean4

theorem mem_top_iff_forall {s : Set α} : s ∈ (⊤ : Filter α) ↔ ∀ x, x ∈ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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