pow_apply — Mathlib

English

For any CauSeq f in β abv and any n ∈ ℕ and i ∈ ℕ, the i-th term of f^n is equal to the i-th term of f raised to the nth power: (f^n)(i) = f(i)^n.

Русский

Для любого CauSeq f в β abv и любого n ∈ ℕ, i ∈ ℕ, i-й член f^n равен i-м члену f в степени n: (f^n)(i) = f(i)^n.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem pow_apply (f : CauSeq β abv) (n i : ℕ) : (f ^ n) i = f i ^ n :=
  rfl

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