coe_sSup_of_directedOn — Mathlib

English

The underlying set of sSup S for directedOn S matches the union across S of the underlying sets.

Русский

Образ множества sSup S по направлению directedOn совпадает с объединением базовых множеств подполь.

LaTeX

$$$\big( \mathrm{sSup}(S) \big) : Set R = \bigcup_{s \in S} (s : Set R)$$$

Lean4

theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubring 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]

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