mem_distinguishedTriangles_iff — Mathlib

English

In opposite categories, a triangle is distinguished if and only if its image under triangleOpEquivalence is distinguished.

Русский

В противоположной категории треугольник является выделенным тогда и только тогда, когда образ под triangleOpEquivalence также является выделенным.

LaTeX

$$$T \in distTriang (C^{op}) \Leftrightarrow (triangleOpEquivalence C)^{-1}.obj T \in distTriang C$$$

Lean4

theorem mem_distinguishedTriangles_iff (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔ ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := by rfl

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