bitraverse

Mathlib.Control.Bitraversable.Instances

URI: https://scilib.ai/kg/mathlib#flip.bitraverse

Lean4

/-- The bitraverse function for `flip`. -/
nonrec def bitraverse {α α' β β'} (f : α → F α') (f' : β → F β') : flip t α β → F (flip t α' β') :=
  (bitraverse f' f : t β α → F (t β' α'))

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

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

Разделы

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

Аффилиация

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