adjoin_union — Mathlib

English

adjoin of a union equals the supremum of adjoin of each set: adjoin_R(s ∪ t) = adjoin_R(s) ⊔ adjoin_R(t).

Русский

adjoin_R(s ∪ t) равно наибольшему соединению adjoin_R(s) и adjoin_R(t).

LaTeX

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

Lean4

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

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