distinguished_iff_of_iso — Mathlib

English

Every morphism Y → Z can be embedded in a distinguished cocone triangle X → Y → Z → X[1].

Русский

Любой морфизм Y → Z можно вставить в выделенный коконовый треугольник X → Y → Z → X[1].

LaTeX

$$distinguished_cocone_triangle₁$$

Lean4

theorem distinguished_iff_of_iso {T₁ T₂ : Triangle C} (e : T₁ ≅ T₂) : T₁ ∈ distTriang C ↔ T₂ ∈ distTriang C :=
  ⟨fun hT₁ => isomorphic_distinguished _ hT₁ _ e.symm, fun hT₂ => isomorphic_distinguished _ hT₂ _ e⟩

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