guitartExact_iff_final — Mathlib

English

A variant of the identity construction yields Guitart exactness.

Русский

Вариант конструирования единичного квадрата дает точность Гитхарта.

LaTeX

$$$\mathrm{GuitartExact}(\mathrm{TwoSquare.mk}(F, \mathrm{id}, \mathrm{id}, F, \mathrm{Id}(F)))$$$

Lean4

theorem guitartExact_iff_final : w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final :=
  ⟨fun _ _ => ⟨fun _ => inferInstance⟩, fun _ => ⟨fun _ => inferInstance⟩⟩

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