coe_iSup_of_directed — Mathlib

English

Let {S_i} be a directed family of nonunital subsemirings of R. Then the carrier of the supremum equals the union of the carriers: ((⨆ i, S_i : NonUnitalSubsemiring R) : Set R) = ⋃ i, (S_i : Set R).

Русский

Пусть {S_i} — направленная семья неединичных подпsemiring R. Тогда носитель верхнего предела равен объединению носителей каждого S_i.

LaTeX

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

Lean4

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

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