zeroIsoIsTerminal_inv

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv

English

The inverse component of the zero initial isomorphism is zero.

Русский

Обратный компонент нулевой начальности равен нулю.

LaTeX

$$(zeroIsoInitial.inv) = 0$$

Lean4

@[simp]
theorem zeroIsoIsTerminal_inv {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).inv = 0 := by ext

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

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

Разделы

Аффилиация

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