length'_ne_zero_iff_cons — Mathlib

English

The nonzeroness of length' implies that the sequence is a nonempty cons: length'(s) ≠ 0 iff ∃ x, ∃ s', s = cons x s'.

Русский

Наличие ненулевой длины' означает существование элемента и последовательности, так что s = cons x s'.

LaTeX

$$$\mathrm{length}'(s) \neq 0 \iff \exists x\, \exists s',\ s = \mathrm{cons}(x, s')$$$

Lean4

theorem length'_ne_zero_iff_cons (s : Seq α) : s.length' ≠ 0 ↔ ∃ x s', s = cons x s' := by cases s <;> simp

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