iterate_pred_comp_of_pos

Mathlib.Logic.Function.Iterate

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

English

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

Русский

Если n > 0, то f^{[n-1]} ∘ f = f^{[n]}. Эквивалентно f ∘ f^{[n-1]} = f^{[n]}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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