mem_distTriang_op_iff — Mathlib

English

A triangle in the opposite category is distinguished iff its image under the triangleOpEquivalence inverse is distinguished in the original category.

Русский

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

LaTeX

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

Lean4

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

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