perm_pow

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.IsFixedPt.perm_pow

English

If x is a fixed point of e, then x is a fixed point of e^n for all n ∈ ℕ.

Русский

Если x фиксирована для e, то x фиксирована и для e^n для всех n∈ℕ.

LaTeX

$$$IsFixedPt e x \rightarrow \forall n:\mathbb{N}, IsFixedPt (e^n) x$$$

Lean4

protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x :=
  h.iterate _

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

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

Разделы

Аффилиация

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