get?_terminates

Mathlib.Data.WSeq.Productive

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.get?_terminates

English

If a weak sequence s is productive, then for every n, the computation get? s n terminates.

Русский

Если слабая последовательность s продуктивна, то для каждого n вычисление get? s n завершается.

LaTeX

$$$$ \forall n,\ (s.\mathrm{get?}\ n).\mathrm{Terminates}. $$$$

Lean4

instance get?_terminates (s : WSeq α) [h : Productive s] : ∀ n, (get? s n).Terminates :=
  h.get?_terminates

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

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

Разделы

Аффилиация

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