pow_apply — Mathlib

English

Let f be a continuous map α → β into a monoid β with continuous multiplication. Then for every n ∈ ℕ and every x ∈ α, (f^n)(x) = (f(x))^n.

Русский

Пусть f — непрерывное отображение α → β в моноид β с непрерывной операцией умножения. Тогда для каждого n ∈ ℕ и каждого x ∈ α выполняется (f^n)(x) = (f(x))^n.

LaTeX

$$$\forall f:\ C(\alpha,\beta),\ \forall n \in \mathbb{N},\ \forall x\in\alpha:\ (f^n)(x) = (f(x))^n.$$$

Lean4

@[to_additive (attr := norm_cast)]
theorem pow_apply [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ℕ) (x : α) : (f ^ n) x = f x ^ n :=
  rfl

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