contractible_distinguished — Mathlib

English

The contractible triangle associated to X ∈ C^op is a distinguished triangle in C.

Русский

Контрактный треугольник, связанный с X ∈ C^op, является выделенным треугольником в C.

LaTeX

$$$\text{contractibleTriangle } X \in distTriang C$$$

Lean4

theorem contractible_distinguished (X : Cᵒᵖ) : contractibleTriangle X ∈ distinguishedTriangles C :=
  by
  rw [mem_distinguishedTriangles_iff']
  exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop), ⟨contractibleTriangleIso X⟩⟩

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