destruct_think

Mathlib.Data.WSeq.Basic

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

← MathLib Explorer

English

Destruct of think s equals think applied to destruct s.

Русский

Destruct от think s равен think от destruct s.

LaTeX

$$$$\mathrm{destruct}(\mathrm{think}(s))= (\mathrm{destruct}(s)).\mathrm{think}.$$$$

Lean4

@[simp]
theorem destruct_think (s : WSeq α) : destruct (think s) = (destruct s).think :=
  Computation.destruct_eq_think <| by simp [destruct, think, Computation.rmap]

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

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

Разделы

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

Аффилиация

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