tsnd_eq_snd_id

Mathlib.Control.Bitraversable.Lemmas

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

Lean4

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

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

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

Разделы

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

Аффилиация

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