pure_traverse

Mathlib.Control.Traversable.Lemmas

URI: https://scilib.ai/kg/mathlib#Traversable.pure_traverse

Lean4

theorem pure_traverse (x : t α) : traverse pure x = (pure x : F (t α)) :=
  by
  have : traverse pure x = pure (traverse (m := Id) pure x) := (naturality (PureTransformation F) pure x).symm
  rwa [id_traverse] at this

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

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

Разделы

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

Аффилиация

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