length_toList — Mathlib

English

For a terminating sequence, the length of its toList representation equals the length of the sequence.

Русский

Для завершающейся последовательности длина списка, полученного через toList, равна длине исходной последовательности.

LaTeX

$$$\mathrm{toList}(s, h).\mathrm{length} = \mathrm{length}(s, h)$$$

Lean4

@[simp]
theorem length_toList (s : Seq α) (h : s.Terminates) : (toList s h).length = length s h :=
  by
  rw [toList, length_take_of_le_length]
  intro _
  exact le_rfl

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