length_eq_zero — Mathlib

English

For terminating sequences, the length is zero if and only if the sequence is nil.

Русский

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

LaTeX

$$$\mathrm{length}(s) = 0 \iff s = \mathrm{nil}$$$

Lean4

@[simp]
theorem length_eq_zero {s : Seq α} {h : s.Terminates} : s.length h = 0 ↔ s = nil := by simp [length, TerminatedAt]

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