comp_snd

Mathlib.Control.Bifunctor

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

Lean4

@[higher_order snd_comp_snd]
theorem comp_snd {α β₀ β₁ β₂} (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α β₀) : snd g' (snd g x) = snd (g' ∘ g) x := by
  simp [snd, bimap_bimap]

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

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

Разделы

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

Аффилиация

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