tfst_eq_fst_id

Mathlib.Control.Bitraversable.Lemmas

URI: https://scilib.ai/kg/mathlib#Bitraversable.tfst_eq_fst_id

Lean4

@[higher_order]
theorem tfst_eq_fst_id {α α' β} (f : α → α') (x : t α β) : tfst (F := Id) (pure ∘ f) x = pure (fst f x) := by
  apply bitraverse_eq_bimap_id

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

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

Разделы

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

Аффилиация

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