map_think

Mathlib.Data.WSeq.Basic

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

English

Applying a map commutes with thinking: map f (think s) = think (map f s).

Русский

Применение отображения коммутирует с операцией think: map f (think s) = think (map f s).

LaTeX

$$$$ \\operatorname{map} f (\\mathrm{think}\\, s) = \\mathrm{think}(\\operatorname{map} f\\, s) $$$$

Lean4

@[simp]
theorem map_think (f : α → β) (s) : map f (think s) = think (map f s) :=
  Seq.map_cons _ _ _

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

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

Разделы

Аффилиация

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