coe_iSup_of_directed — Mathlib

English

The coerce of the iSup over i of submonoids equals the union of the coerced submonoids: ((⨆ i, S_i) : Set M) = ⋃ i, S_i.

Русский

Образ iSup над i подпомонидами равен объединению их изображений: ((⨆ i, S_i) : Set M) = ⋃ i, S_i.

LaTeX

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

Lean4

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

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