length'_eq_zero_iff_nil

Mathlib.Data.Seq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.length'_eq_zero_iff_nil

English

The length' of a sequence is zero exactly when the sequence is nil.

Русский

Длина' последовательности равна нулю тогда и только тогда, когда последовательность равна nil.

LaTeX

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

Lean4

@[simp]
theorem length'_eq_zero_iff_nil (s : Seq α) : s.length' = 0 ↔ s = nil := by cases s <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru