think_equiv

Mathlib.Data.WSeq.Relation

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

English

For any s, think s is equivalent to s.

Русский

Для любой последовательности s, think s эквивалентно s.

LaTeX

$$$\forall s:\mathrm{WSeq}(\alpha),\ \mathrm{think}\,s \sim_W s$$$

Lean4

theorem think_equiv (s : WSeq α) : think s ~ʷ s := by unfold Equiv; simpa using Equiv.refl _

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

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

Разделы

Аффилиация

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