English
If a monoid α acts on a type β, then β-power set (the collection of all subsets of β) carries a natural action of α given by a • S = {a • x | x ∈ S}. This defines a multiplicative action of α on Set β, satisfying (ab) • S = a • (b • S) and 1 • S = S for all a,b in α and S ⊆ β.
Русский
Пусть моноид α действует на множество β. Тогда множество подмножеств β образует естественное действие α: для a ∈ α и подмножества S ⊆ β определяем a • S = {a • x | x ∈ S}. Это задаёт действие α на Set β, удовлетворяющее (ab) • S = a • (b • S) и 1 • S = S для всех a,b ∈ α и S ⊆ β.
LaTeX
$$$\forall a,b \in \alpha, \forall S \subseteq \beta:\ (ab)\cdot S = a\cdot(b\cdot S) \quad\text{and}\quad 1\cdot S = S, \quad \text{where } a\cdot S = \{a\cdot x : x \in S\}. $$$
Lean4
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Set β`. -/
@[to_additive /-- An additive action of an additive monoid on a type `β` gives an additive action on `Set β`. -/
]
protected def mulActionSet [Monoid α] [MulAction α β] : MulAction α (Set β)
where
mul_smul _ _ _ := by simp only [← image_smul, image_image, ← mul_smul]
one_smul _ := by simp only [← image_smul, one_smul, image_id']
