binaryProductTriangle_distinguished

English

A chosen extension of a commutative square into a morphism of distinguished triangles exists.

Русский

Существование выбранного продолжения коммутативного квадрата в морфизм между распознаваемыми треугольниками.

LaTeX

$$$\\exists \\phi : T_1 \\to T_2, \\ \\text{ s.t. } \\text{commutative relations hold}$$$

Lean4

theorem binaryProductTriangle_distinguished (X₁ X₂ : C) : binaryProductTriangle X₁ X₂ ∈ distTriang C :=
  isomorphic_distinguished _ (binaryBiproductTriangle_distinguished X₁ X₂) _
    (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂)

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