mem_sSup_of_directed_on — Mathlib

English

Let S be a directed family (with respect to inclusion) of subsemigroups of a semigroup M. Then for every element x in M, x belongs to the supremum of S if and only if x belongs to some member of S.

Русский

Пусть S — направленное по включению семейство подполугрупп в полугруппе M. Тогда для всякого элемента x ∈ M выполняется: x принадлежит верхней границе (supremum) S тогда и только тогда, когда x принадлежит какой-либо подмножеству из S.

LaTeX

$$$x \\in \\operatorname{sSup} S \\iff \\exists s \\in S, x \\in s$$$

Lean4

@[to_additive]
theorem mem_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) {x : M} :
    x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

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