toList_terminates

Mathlib.Data.WSeq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.toList_terminates

English

If s is finite, then toList s terminates.

Русский

Если s конечна, то toList s заканчивается.

LaTeX

$$$$ s.\\text{IsFinite} \\Rightarrow (\\text{toList } s).\\text{Terminates} $$$$

Lean4

instance toList_terminates (s : WSeq α) [h : IsFinite s] : (toList s).Terminates :=
  h.out

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

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

Разделы

Аффилиация

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