coe_pow — Mathlib

English

The evaluation map commutes with exponentiation: the underlying function of f^n equals the pointwise nth power of the underlying function, i.e. the nth power is taken termwise.

Русский

Оценочное отображение сохраняет возведение в степень: базовая функция f^n равна покомпонентно возведённой в степень n функции f.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_pow (f : CauSeq β abv) (n : ℕ) : ⇑(f ^ n) = (f : ℕ → β) ^ n :=
  rfl

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