mem_sSup_of_directedOn — Mathlib

English

For directedOn S ⊆ Set(Subring R) with Sne.Nonempty, x ∈ sSup S iff ∃ s ∈ S, x ∈ s.

Русский

Для directedOn S ⊆ Set(Subring R) с Sne.Nonempty, x ∈ sSup S тогда и только тогда, когда ∃ s ∈ S, x ∈ s.

LaTeX

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

Lean4

theorem mem_sSup_of_directedOn {S : Set (Subring 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]

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