infty_coeFn_pow — Mathlib

English

If f is an element of the ∞-normed space, then its n-th power agrees with taking the n-th power coordinatewise on each index.

Русский

Если f принадлежит пространству ∞-нормы, то его n-я степень совпадает с поиндексному возведением в степень в каждой координате.

LaTeX

$$$\bigl( f^n \bigr)(i) = \bigl( f(i) \bigr)^n \quad\text{for all } i,$$$

Lean4

@[simp]
theorem infty_coeFn_pow (f : lp B ∞) (n : ℕ) : ⇑(f ^ n) = (⇑f) ^ n :=
  rfl

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