instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact

Mathlib.CategoryTheory.GuitartExact.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact

English

For any X2, the downward structured arrow is initial.

Русский

Для любого X2 нижняя структурированная стрелка является начальнoй.

LaTeX

$$$(\mathrm{structuredArrowDownwards}\, X_2).\mathrm{Initial}$$$

Lean4

instance [hw : w.GuitartExact] (X₂ : C₂) : (w.structuredArrowDownwards X₂).Initial :=
  by
  rw [guitartExact_iff_initial] at hw
  apply hw

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

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

Разделы

Аффилиация

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