toList_node — Mathlib

English

The toList of a node is the concatenation of the left toList, the node's value, and the right toList: toList(node(s, l, x, r)) = toList(l) ++ x :: toList(r).

Русский

toList узла равно toList левого поддерева, затем значение x, затем toList правого поддерева: toList(node(s, l, x, r)) = toList(l) ++ x :: toList(r).

LaTeX

$$toList(\mathrm{node}(s, l, x, r)) = toList(l) \; +\; (x \,::\, toList(r))$$

Lean4

@[simp]
theorem toList_node (s l x r) : toList (@node α s l x r) = toList l ++ x :: toList r := by
  rw [toList, foldr, foldr_cons_eq_toList]; rfl

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