mem_sSup_iff — Mathlib

English

For any set S of upper sets, an element a belongs to the supremum sSup S iff a belongs to every member of S.

Русский

Для множества S верхних множеств элемент a принадлежит наименьшему верхнему пределу sSup S тогда, когда он принадлежит каждому элементу S.

LaTeX

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

Lean4

@[simp]
theorem mem_sSup_iff : a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s :=
  mem_iInter₂

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