English
Copying a subsemigroup S to a new carrier s with hs gives a subsemigroup whose carrier is s and whose multiplication is transported from S via hs.
Русский
Копирование подполугруппы S в новую носитель s с hs образует подполугруппу с носителем s и умножением, перенесенным из S через hs.
LaTeX
$$$ \operatorname{carrier}(S.copy(s, hs)) = s \quad\land\quad \forall a,b \in s, a b \in s $$$
Lean4
/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/
@[to_additive /-- Copy an additive subsemigroup replacing `carrier` with a set that is equal to it. -/
]
protected def copy (S : Subsemigroup M) (s : Set M) (hs : s = S) : Subsemigroup M
where
carrier := s
mul_mem' := hs.symm ▸ S.mul_mem'
