coe_sSup_of_directed_on — Mathlib

English

Assume S is a directed family of subsemigroups of M. Then the carrier set of the supremum sSup S equals the union of the carrier sets of all s in S.

Русский

Пусть S направленное семейство подполугрупп в M. Тогда множество-носитель верхнего предела sSup S равно объединению носителей всех S в S.

LaTeX

$$$(\\uparrow(\\operatorname{sSup} S) : \\; \\text{Set } M) = \\bigcup_{s \\in S} \\uparrow s$$$

Lean4

@[to_additive]
theorem coe_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) :
    (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directed_on hS]

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