coe_sSup_of_directedOn — Mathlib

English

For directedOn S, the carrier of the supremum equals the union of carriers: ↑(sSup S) = ⋃ s ∈ S, ↑s.

Русский

Для directedOn S, носитель sSup S равен объединению носителей: ↑(sSup S) = ⋃ s ∈ S, ↑s.

LaTeX

$$$ ↑(sSup S) = \bigcup_{s \in S} ↑s $$$

Lean4

theorem coe_sSup_of_directedOn {S : Set (Subring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) :
    (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

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