coe_iSup_of_directed — Mathlib

English

If (S_i) is a directed family of NonUnitalSubring R indexed by ι, then the underlying set of iSup_i S_i equals the union across i of the underlying sets S_i.

Русский

Для направленного семейства подполь в R, каркас-объединение iSup_i S_i имеет множество равное объединению множеств S_i.

LaTeX

$$$((\iSup i, S_i) : NonUnitalSubring R) : Set R = \bigcup_i S_i$$$

Lean4

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

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