NPow — Mathlib

English

There is a natural-number power operation on Set α defined by S^n as the n-fold pointwise product of S.

Русский

Существует возведение множества в натуральную степень: S^n задаёт n-кратное точечное произведение множества S.

LaTeX

$$$$ S^n = \{ a_1 \cdots a_n \mid a_i \in S \}, \quad S^0 = \{1\}. $$$$

Lean4

/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Set`. See note [pointwise nat action]. -/
@[to_additive existing]
protected def NPow [One α] [Mul α] : Pow (Set α) ℕ :=
  ⟨fun s n => npowRec n s⟩

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