coe_iSup_of_directed — Mathlib

English

Under a directed family hS, the underlying set of iSup S i equals the union over i of S i.

Русский

При направленном семейство hS предельный элемент iSup имеет множество элементов, совпадающих с объединением ⋃_i S_i.

LaTeX

$$$ ((\\iSup i, S i) : Subsemigroup M) : Set M = \\bigcup i, S i $$$

Lean4

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

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