instPowNat — Mathlib

English

Let f be a CauSeq in β with abv. For every natural number n, the nth power f^n is defined by taking powers termwise: (f^n)(i) = f(i)^n for all i ∈ ℕ.

Русский

Пусть f — CauSeq в β с abv. Для каждого натурального числа n определяется степенная последовательность f^n по каждому члену: (f^n)(i) = f(i)^n для всех i ∈ ℕ.

LaTeX

$$$\forall n \in \mathbb{N}, \forall i \in \mathbb{N}, (f^n)(i) = f(i)^n$$$

Lean4

instance : Pow (CauSeq β abv) ℕ :=
  ⟨fun f n => (ofEq (npowRec n f) fun i => f i ^ n) <| by induction n <;> simp [*, npowRec, pow_succ]⟩

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