productive_congr

Mathlib.Data.WSeq.Productive

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

← MathLib Explorer

English

For any sequence s in the Stream'.Seq type, (WSeq.ofSeq s) is productive.

Русский

Для любой последовательности s типа Stream'.Seq, (WSeq.ofSeq s) продуктивна.

LaTeX

$$$$ (\mathrm{WSeq}.\mathrm{ofSeq}\ s).\mathrm{Productive}. $$$$

Lean4

theorem productive_congr {s t : WSeq α} (h : s ~ʷ t) : Productive s ↔ Productive t := by simp only [productive_iff];
  exact forall_congr' fun n => terminates_congr <| get?_congr h _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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