length_toList — Mathlib

English

Let t be a Sized Ordnode α. Then the length of the list obtained by converting t to a list equals the size of t.

Русский

Пусть t — упорядоченное дерево Ordnode над α, удовлетворяющее условию Sized. Тогда длина списка, полученного преобразованием t в список, равна размеру t.

LaTeX

$$$|\operatorname{toList}(t)| = \operatorname{size}(t)$$$

Lean4

theorem length_toList {t : Ordnode α} (h : Sized t) : (toList t).length = t.size := by
  rw [length_toList', size_eq_realSize h]

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