NSMul — Mathlib

English

There is a natural action of the natural numbers on the collection of subsets of α given by n-fold pointwise addition.

Русский

Существует естественное действие множества ℕ на множества подмножеств α, задаваемое n-кратовым поэлементным сложением.

LaTeX

$$$$ n \cdot S = \begin{cases} \{0\} & n=0 \\\\ \{ x_1 + \cdots + x_n \mid x_i \in S \} & n>0 \end{cases} \quad (S \subseteq \alpha) $$$$

Lean4

/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Set`. See
note [pointwise nat action]. -/
protected def NSMul [Zero α] [Add α] : SMul ℕ (Set α) :=
  ⟨nsmulRec⟩

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