adjoin_union — Mathlib

English

The algebra generated by the union of two sets s and t is the join of the algebras generated by each set individually: adjoin_R(s ∪ t) = adjoin_R(s) ⊔ adjoin_R(t).

Русский

Порождение над R множества s ∪ t равно объединению порождений отдельных множеств: adjoin_R(s ∪ t) = adjoin_R(s) ⊔ adjoin_R(t).

LaTeX

$$$$\\operatorname{adjoin}_R(s \\cup t) = \\operatorname{adjoin}_R(s) \\;\\amalg\\; \\operatorname{adjoin}_R(t)$$$$

Lean4

theorem adjoin_union (s t : Set A) : adjoin R (s ∪ t) = adjoin R s ⊔ adjoin R t :=
  (Algebra.gc : GaloisConnection _ ((↑) : Subalgebra R A → Set A)).l_sup

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