mem_sSup_of_directedOn — Mathlib

English

If S is a directed family of submonoids of M, then x ∈ sSup S iff there exists some s ∈ S with x ∈ s.

Русский

Если S направленное семейство подпомонид, то x ∈ sSup S тогда и только тогда, когда существует s ∈ S с x ∈ s.

LaTeX

$$$x \in sSup S \iff \exists s \in S, x \in s$$$

Lean4

@[to_additive]
theorem mem_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : M} :
    x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  haveI : Nonempty S := Sne.to_subtype
  simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val]

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