inr_f_desc_f

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

URI: https://scilib.ai/kg/mathlib#CochainComplex.mappingCone.inr_f_desc_f

English

If α = α' and β = β' and eq and h' and other data are equal, then the desc φ α β eq equals desc φ α' β' eq.

Русский

Если α = α' и β = β' иEq и прочие данные равны, то desc φ α β eq = desc φ α' β' eq.

LaTeX

$$$\text{Eq}(\desc(φ, α, β, eq), \desc(φ, α', β', eq))$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_f_desc_f (p : ℤ) : (inr φ).f p ≫ (desc φ α β eq).f p = β.f p := by simp [desc]

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

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

Разделы

Аффилиация

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