comp_fst

Mathlib.Control.Bifunctor

URI: https://scilib.ai/kg/mathlib#Bifunctor.comp_fst

Lean4

@[higher_order fst_comp_fst]
theorem comp_fst {α₀ α₁ α₂ β} (f : α₀ → α₁) (f' : α₁ → α₂) (x : F α₀ β) : fst f' (fst f x) = fst (f' ∘ f) x := by
  simp [fst, bimap_bimap]

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

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

Разделы

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

Аффилиация

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