foldr_cons_eq_toList — Mathlib

English

For any tree t and list r, t.foldr(List.cons) r equals toList(t) ++ r.

Русский

Для любого дерева t и списка r выполняется t.foldr(List.cons) r = toList(t) ++ r.

LaTeX

$$∀ t r, t.foldr List.cons r = toList t ++ r$$

Lean4

theorem foldr_cons_eq_toList : ∀ (t : Ordnode α) (r : List α), t.foldr List.cons r = toList t ++ r
  | nil, _ => rfl
  | node _ l x r, r' => by
    rw [foldr, foldr_cons_eq_toList l, foldr_cons_eq_toList r, ← List.cons_append, ← List.append_assoc, ←
      foldr_cons_eq_toList l];
    rfl

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