pow_apply — Mathlib

English

Let R be a monoid with bounded and continuous multiplication. For every natural n and every bounded continuous function f: α →ᵇ R, and every x ∈ α, the nth power of f evaluated at x equals the nth power of f(x): (f^n)(x) = f(x)^n.

Русский

Пусть R — моноид с ограничиваемым и непрерывным умножением. Для любого натурального n и любой ограниченной непрерывной функции f: α →ᵇ R и для каждого x ∈ α выполняется (f^n)(x) = f(x)^n.

LaTeX

$$$\forall n \in \mathbb{N},\; \forall f \in C_b(\alpha, R),\; \forall x \in \alpha:\ (f^n)(x) = f(x)^n$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_apply [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ℕ) (f : α →ᵇ R) (x : α) : (f ^ n) x = f x ^ n :=
  rfl

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