foldr_eta — Mathlib

English

For any list l, folding with the constructor cons starting from the empty list reproduces the original list: foldr cons [] l = l.

Русский

Для любого списка l свёртка через конструктор cons с пустым основанием восстанавливает исходный список: foldr cons [] l = l.

LaTeX

$$$$\\operatorname{foldr}(\\text{cons})\\, \\emptyset \\, l = l.$$$$

Lean4

@[deprecated foldr_cons_nil (since := "2025-02-10")]
theorem foldr_eta (l : List α) : foldr cons [] l = l :=
  foldr_cons_nil

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