coe_pow

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.coe_pow

English

For any f ∈ CircleDeg1Lift and n ∈ ℕ, the coercion of f^n equals the nth iterate of f.

Русский

Для любого f ∈ CircleDeg1Lift и n ∈ ℕ коэрцирование f^n равно n-й итерации f.

LaTeX

$$$\\forall f \\in CircleDeg1Lift,\\ \\forall n \\in \\mathbb{N},\\ \\text{coer}(f^n) = f^{[n]}$$$

Lean4

theorem coe_pow : ∀ n : ℕ, ⇑(f ^ n) = f^[n]
  | 0 => rfl
  | n + 1 => by simp [coe_pow n, pow_succ]

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

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

Разделы

Аффилиация

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