mem_distTriang_op_iff' — Mathlib

English

A refinement: there exists a distinguished-triangle data in C corresponding to T in C^op with a nonempty isomorphism after applying triangleOpEquivalence.

Русский

Уточнение: существует соответствие между данными выделенного треугольника в C и T в C^op через не пустой изоморфизм после применения triangleOpEquivalence.

LaTeX

$$$(T \in distTriang C^{op}) \iff \exists T', T' \in distTriang C, \; Nonempty (T \cong (triangleOpEquivalence C).functor.obj (Opposite.op T'))$$$

Lean4

theorem mem_distTriang_op_iff' (T : Triangle Cᵒᵖ) :
    (T ∈ distTriang Cᵒᵖ) ↔
      ∃ (T' : Triangle C) (_ : T' ∈ distTriang C),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')) :=
  Opposite.mem_distinguishedTriangles_iff' T

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