ext_r

Mathlib.Algebra.Homology.ShortComplex.Exact

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

← MathLib Explorer

English

Two splittings with equal r map are equal.

Русский

Две расщепления с равным отображением r совпадают.

LaTeX

$$s.r = s'.r \Rightarrow s = s'$$

Lean4

theorem ext_r (s s' : S.Splitting) (h : s.r = s'.r) : s = s' :=
  by
  have := s.epi_g
  have eq := s.id
  rw [← s'.id, h, add_right_inj, cancel_epi S.g] at eq
  cases s
  congr

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

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

Разделы

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

Аффилиация

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