hom_ext₄ — Mathlib

English

For four-step arrows, equality on all five app' components implies equality of the morphisms.

Русский

Для четырехступенчатых стрел равенство всех пяти компонент app' -> равенство морфизмов.

LaTeX

$$$\\forall {f,g}:{\\text{ComposableArrows}}~C~4,\\; (h_0,h_1,h_2,h_3,h_4) : (app' φ i)=(app' φ' i)\\ (i=0..4) \\Rightarrow φ=φ'$$$

Lean4

@[ext]
theorem hom_ext₄ {f g : ComposableArrows C 4} {φ φ' : f ⟶ g} (h₀ : app' φ 0 = app' φ' 0) (h₁ : app' φ 1 = app' φ' 1)
    (h₂ : app' φ 2 = app' φ' 2) (h₃ : app' φ 3 = app' φ' 3) (h₄ : app' φ 4 = app' φ' 4) : φ = φ' :=
  hom_ext_succ h₀ (hom_ext₃ h₁ h₂ h₃ h₄)

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