ι₀_desc

Mathlib.Algebra.Homology.HomotopyCofiber

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.cylinder.ι₀_desc

English

In the cylinder construction, the projection ι₀ composed with desc φ₀ φ₁ h gives φ₀.

Русский

В цилиндрическом конструировании проекция ι₀, применённая к desc φ₀ φ₁ h, даёт φ₀.

LaTeX

$$$ ι₀ K \\;\\gg\\; desc φ₀ φ₁ h = φ₀. $$$

Lean4

@[reassoc (attr := simp)]
theorem ι₀_desc : ι₀ K ≫ desc φ₀ φ₁ h = φ₀ := by simp [ι₀, desc]

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

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

Разделы

Аффилиация

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