coe_iSup_of_directed — Mathlib

English

The underlying set of the supremum iSup_i S_i equals the union ⋃ i, S_i.

Русский

Множество, содержащее iSup_i S_i, образует объединение ⋃ i S_i.

LaTeX

$$$((\\bigsqcup_i S_i) : Set\\ R) = \\bigcup_i S_i$$$

Lean4

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

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