English
Let R be a commutative semiring and A a nonunital star algebra over R. For any subset s of A, adjoin R s denotes the smallest nonunital star subalgebra of A that contains s.
Русский
Пусть R — коммутативное полукольцо, A — ненулевая звездная подпалгебра над R. Для множества s ⊆ A обозначение adjoin R s означает наименьшую ненулеподпалгебру без единицы в A, содержащую s.
LaTeX
$$$\\\\operatorname{adjoin}_R(s) = \\bigcap\\\\{T \\\\subseteq A \\mid T \\text{ is a NonUnitalStarSubalgebra and } s \\subseteq T\\\\}$$$
Lean4
/-- The minimal non-unital subalgebra that includes `s`. -/
def adjoin (s : Set A) : NonUnitalStarSubalgebra R A
where
toNonUnitalSubalgebra := NonUnitalAlgebra.adjoin R (s ∪ star s)
star_mem'
_ := by
rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff, NonUnitalSubalgebra.star_adjoin_comm,
Set.union_star, star_star, Set.union_comm]
