instZPow — Mathlib

English

If β is a group with IsTopologicalGroup, then Pow C(α,β) Int is defined by (f^z)(x) = (f(x))^z for z ∈ ℤ and x ∈ α.

Русский

Если β — группа с IsTopologicalGroup, то пространство непрерывных отображений C(α,β) имеет Z-возведение: (f^z)(x) = (f(x))^z для z ∈ ℤ и x ∈ α.

LaTeX

$$$\forall f:\ C(\alpha,\beta),\forall z∈\mathbb{Z}: (f^z)(x) = (f(x))^z\text{ для всех } x. $$$

Lean4

@[to_additive existing]
instance instZPow [Group β] [IsTopologicalGroup β] : Pow C(α, β) ℤ where pow f z := ⟨(⇑f) ^ z, f.continuous.zpow z⟩

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