mem_sSup_of_directedOn — Mathlib

English

If S is a nonempty directed set of substructures of M, then x belongs to the supremum sSup S if and only if there exists some s ∈ S with x ∈ s.

Русский

Пусть S — ненулевое направленное множество подструктур M. Тогда элемент x принадлежит наибольшему верхнему пределу sSup S тогда и только тогда, когда существует s ∈ S такое, что x ∈ s.

LaTeX

$$$x \\in \\mathrm{sSup}\\, S \\;\\Longleftrightarrow\\; \\exists s \\in S, x \\in s$$$

Lean4

theorem mem_sSup_of_directedOn {S : Set (L.Substructure M)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : M} :
    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]

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