instPow — Mathlib

English

There is a power operation on ContinuousMap α β by natural exponents: f^n is defined pointwise with continuous n-th power.

Русский

Существует операция возведения в степень для непрерывных отображений: f^n определяется по точкам как f(x)^n и непрерывно.

LaTeX

$$ [Monoid β] [ContinuousMul β] : Pow (ContinuousMap α β) Nat$$

Lean4

@[to_additive existing]
instance instPow [Monoid β] [ContinuousMul β] : Pow C(α, β) ℕ :=
  ⟨fun f n => ⟨(⇑f) ^ n, f.continuous.pow n⟩⟩

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