length_cons — Mathlib

English

If s terminates, then the length of the sequence obtained by cons x s equals the length of s plus one.

Русский

Если последовательность s завершается, то длина последовательности, полученной добавлением элемента x к голове, равна длине s плюс единица.

LaTeX

$$$\operatorname{length}(\mathrm{cons}(x, s)) = \operatorname{length}(s) + 1$$$

Lean4

theorem length_cons {x : α} {s : Seq α} (h : s.Terminates) :
    (cons x s).length (terminates_cons_iff.mpr h) = s.length h + 1 :=
  by
  apply Nat.find_comp_succ
  simp

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