length'_nil

Mathlib.Data.Seq.Basic

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

English

The modified length of the empty sequence is 0.

Русский

Упрощенная (length') длина пустой последовательности равна 0.

LaTeX

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

Lean4

@[simp]
theorem length'_nil : length' (nil : Seq α) = 0 := by simp -implicitDefEqProofs [length']

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

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

Разделы

Аффилиация

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