sSup_def — Mathlib

English

The supremum sSup S of a set S of subalgebras equals the subalgebra generated by the union of their underlying sets.

Русский

Надмножество (область) верхнего предела sSup S эквивалентно порожденной подалгебре от объединения соответствующих множеств.

LaTeX

$$$\mathrm{sSup}\;S = \mathrm{adjoin}_R\left(\bigcup\_{S_i\in S} S_i\right)$$$

Lean4

theorem sSup_def (S : Set (Subalgebra R A)) : sSup S = adjoin R (⋃₀ (SetLike.coe '' S)) :=
  rfl

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