opcycles_ext

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.opcycles_ext

← MathLib Explorer

English

If S.pOpcycles ∘ f1 = S.pOpcycles ∘ f2, then f1 = f2.

Русский

Если pOpcycles ∘ f1 = pOpcycles ∘ f2, тогда f1 = f2.

LaTeX

$$$ S.pOpcycles \circ f_1 = S.pOpcycles \circ f_2 \Rightarrow f_1 = f_2 $$$

Lean4

@[ext]
theorem opcycles_ext {A : C} (f₁ f₂ : S.opcycles ⟶ A) (h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂) : f₁ = f₂ := by
  simpa only [opcycles_ext_iff]

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

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

Разделы

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

Аффилиация

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