join_ret

Mathlib.Data.WSeq.Relation

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

English

For every s, join (ret s) is weakly equivalent to s: join (ret s) ~ʷ s.

Русский

Для любой последовательности s: join (ret s) эквивалентна s в слабом смысле.

LaTeX

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

Lean4

@[simp]
theorem join_ret (s : WSeq α) : join (ret s) ~ʷ s := by simpa [ret] using think_equiv _

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

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

Разделы

Аффилиация

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