comp_iterate_pred_of_pos

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.comp_iterate_pred_of_pos

English

If n > 0, then f ∘ f^{[n-1]} = f^{[n]}.

Русский

Если n > 0, то f ∘ f^{[n-1]} = f^{[n]}.

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall n>0,\ f\circ f^{[n-1]} = f^{[n]}. $$$$

Lean4

theorem comp_iterate_pred_of_pos {n : ℕ} (hn : 0 < n) : f ∘ f^[n.pred] = f^[n] := by
  rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]

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

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

Разделы

Аффилиация

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