L₀X₂ToP_comp_pullback_snd

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd

English

The composite L₀X₂ToP with pullback.snd equals L₀.g.

Русский

Сложение L₀X₂ToP с pullback.snd равно L₀.g.

LaTeX

$$$S.L_0X_2ToP \circ \mathrm{pullback.snd}(S.L_1.g, S.v_{01}.\\tau_3) = S.L_0.g$$$

Lean4

@[reassoc]
theorem L₀X₂ToP_comp_pullback_snd : S.L₀X₂ToP ≫ pullback.snd _ _ = S.L₀.g := by simp

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

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

Разделы

Аффилиация

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