someOctahedron — Mathlib

English

There is a further octahedron associated canonically to isomorphic triangles.

Русский

Существует дополнительный октaэдр, канонически связанный с изоморфными треугольниками.

LaTeX

$$$\\text{ofIso} : \\text{Given isomorphisms, produce an octahedron for the target triangle}$$$

Lean4

/-- A choice of octahedron given by the octahedron axiom. -/
def someOctahedron [IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
    (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ X₁⟦(1 : ℤ)⟧} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distTriang C)
    {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ X₂⟦(1 : ℤ)⟧} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distTriang C) {v₁₃ : X₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ X₁⟦(1 : ℤ)⟧} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distTriang C) : Octahedron comm h₁₂ h₂₃ h₁₃ :=
  someOctahedron' _

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