instContainsIdentitiesTrWOfContainsZero

Mathlib.CategoryTheory.Triangulated.Subcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instContainsIdentitiesTrWOfContainsZero

← MathLib Explorer

English

Equality of trW under isoClosure: P.isoClosure.trW = P.trW.

Русский

Согласование трW для isoClosure: P.isoClosure.trW = P.trW.

LaTeX

$$$P.isoClosure.trW = P.trW$$$

Lean4

instance [P.ContainsZero] : P.trW.ContainsIdentities :=
  by
  rw [← trW_isoClosure]
  exact ⟨fun X => ⟨_, _, _, contractible_distinguished X, prop_zero _⟩⟩

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

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

Разделы

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

Аффилиация

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