φ_snd

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.kernelCokernelCompSequence.φ_snd

English

The second leg of φ is compatible with the second projection.

Русский

Вторая ножка φ совместима с второй проекцией.

LaTeX

$$φ f g \circ biprod.snd = biprod.snd \circ g$$

Lean4

@[reassoc (attr := simp)]
theorem φ_snd : φ f g ≫ biprod.snd = biprod.snd ≫ g := by
  dsimp [φ]
  aesop

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

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

Разделы

Аффилиация

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