restrictionToTruncGE'_hasLift

Mathlib.Algebra.Homology.Embedding.TruncGE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.restrictionToTruncGE'_hasLift

Lean4

theorem restrictionToTruncGE'_hasLift : e.HasLift (K.restrictionToTruncGE' e) :=
  by
  intro j hj i' _
  dsimp [restrictionToTruncGE']
  rw [restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv K e rfl hj]
  simp [restrictionXIso]

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

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

Разделы

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

Аффилиация

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