coe_iSup_of_directed — Mathlib

English

For directedOn S ⊆ Subring R, the underlying set of the sSup equals the union of the underlying sets: ↑(sSup S) = ⋃ s ∈ S, ↑s.

Русский

Для directedOn S ⊆ Subring R, множество sSup(S) равно объединению множеств ↑s.

LaTeX

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

Lean4

theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

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