mem_sSup

Mathlib.Order.Filter.Defs

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

English

A set s belongs to the supremum of S exactly when s belongs to every filter in S.

Русский

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

LaTeX

$$$s \\in \\operatorname{sSup} S \\iff \\forall f \\in S, s \\in f$$$

Lean4

@[simp]
theorem mem_sSup {S : Set (Filter α)} : s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f :=
  .rfl

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

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

Разделы

Аффилиация

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