iterateTR_loop_eq — Mathlib

English

For any f, a, n, and list l, the loop iteration is equal to reversing l and then appending the standard iterate list.

Русский

Для любого f, a, n и списка l последовательность iterateTR.loop f a n l равна обратному списку l, дополненному iterate f a n.

LaTeX

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

Lean4

theorem iterateTR_loop_eq (f : α → α) (a : α) (n : ℕ) (l : List α) :
    iterateTR.loop f a n l = reverse l ++ iterate f a n := by induction n generalizing a l <;> simp [*]

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