unop_distinguished — Mathlib

English

Let T be a distinguished triangle in the opposite category Cᵒᵖ. Then, after applying the inverse part of the opposite triangle equivalence and unop, the resulting triangle is distinguished in C.

Русский

Пусть T — выделенный треугольник в Cᵒᵖ. Применив обратную часть противоположительной эквивалентности треугольников и применив unop, получившийся треугольник является выделенным в C.

LaTeX

$$$((\\triangleOpEquivalence C).inverse.obj T).unop \\in distTriang\\; C$$$

Lean4

theorem unop_distinguished (T : Triangle Cᵒᵖ) (hT : T ∈ distTriang Cᵒᵖ) :
    ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C :=
  hT

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