homMk₅_app_four — Mathlib

English

The construction isoMk5 provides an isomorphism f ≅ g given isomorphisms at each vertex and commuting squares.

Русский

Конструктор isoMk5 задаёт изоморфизм f ≅ g при наличии изоморфизмов вершин и числовых диаграмм-коммутировок.

LaTeX

$$$\forall f,g : ComposableArrows C 5\; (app_0 : f.obj' 0 \cong g.obj' 0)\dots (app_5 : f.obj' 5 \cong g.obj' 5)\; (w_0:\; f.map' 0 1 ≫ app_1.hom = app_0.hom ≫ g.map' 0 1) \dots (w_4:\; f.map' 4 5 ≫ app_5.hom = app_4.hom ≫ g.map' 4 5) \Rightarrow f \cong g$$$

Lean4

@[simp]
theorem homMk₅_app_four : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, by valid⟩ = app₄ :=
  rfl

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