mem_sSup_of_directedOn — Mathlib

English

Let S be a directedOn subset of NonUnitalSubsemiring R. Then x ∈ sSup S if and only if there exists s ∈ S with x ∈ s.

Русский

Пусть S ⊆ NonUnitalSubsemiring R направлена по отношению ⩽. Тогда x ∈ sSup S тогда же, когда существует s ∈ S такое, что x ∈ s.

LaTeX

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

Lean4

theorem mem_sSup_of_directedOn {S : Set (NonUnitalSubsemiring 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, Subtype.exists, exists_prop]

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