reverse_foldl — Mathlib

English

If you build a list by repeatedly prepending the current element using foldl (t,h) -> h :: t starting with [], then reversing the result yields the original list: reverse (foldl (fun t h => h :: t) [] l) = l.

Русский

Если построить список слева, последовательно добавляя элементы слева через foldl (t,h) → h :: t, начиная с [], то обращение полученного списка возвращает исходный список: reverse (foldl (λ t h. h :: t) [] l) = l.

LaTeX

$$$$\operatorname{reverse}(\operatorname{foldl}(\lambda t\, h. h:\, t)\, []\, l) = l.$$$$

Lean4

theorem reverse_foldl {l : List α} : reverse (foldl (fun t h => h :: t) [] l) = l := by simp

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