mem_sSup_of_directedOn — Mathlib

English

For any directedOn set S of NonUnitalSubring R, x ∈ sSup S iff ∃ s ∈ S, x ∈ s.

Русский

Для направленного множества S подполь в R верно: x ∈ sSup S ⇔ ∃ s ∈ S, x ∈ s.

LaTeX

$$$x \in \mathrm{sSup}(S) \iff \exists s \in S, x \in s$$$

Lean4

theorem mem_sSup_of_directedOn {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : R} :
    x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  haveI : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

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