mem_sSup_of_directedOn — Mathlib

English

For a directed set S of subfields of K, the membership in sSup S is equivalent to x lying in some member of S.

Русский

Для направленного множества S подполей K принадлежность x sSup S равносильна тому, что x принадлежит какому–либо элементу S.

LaTeX

$$$ x \in \operatorname{sSup} S \iff \exists s \in S, x \in s $$$

Lean4

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

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