instPowNat

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.instPowNat

English

There is a natural-number power structure on α →ₘ[μ] γ, i.e., f^n defined for natural n.

Русский

Существует структура возведения в натуральную степень на α →ₘ[μ] γ, т.е. f^n определено для n ∈ ℕ.

LaTeX

$$$ f^{n} \in (α \to_{μ} γ) $ for all n ∈ ℕ$$

Lean4

instance instPowNat : Pow (α →ₘ[μ] γ) ℕ :=
  ⟨fun f n => comp _ (continuous_pow n) f⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru