iterate_eq_iterateTR — Mathlib

English

The ordinary iteration procedure and the specialized List.iterateTR coincide as functions of f, a, n.

Русский

Периодическая процедура итерации и специализированная List.iterateTR совпадают как функции от f, a, n.

LaTeX

$$$\forall f:\, \alpha \to \alpha,\; a:\, \alpha,\; n:\, \mathbb{N},\; List.iterate\; f\ a\ n = List.iterateTR\; f\ a\ n$$$

Lean4

@[csimp]
theorem iterate_eq_iterateTR : @iterate = @iterateTR :=
  by
  funext α f a n
  exact Eq.symm <| iterateTR_loop_eq f a n []

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