hom_ext₂ — Mathlib

English

In the 2-length case, the component at index 2 of homMk₂ is precisely app2.

Русский

В ситуации длины 2 компонент на позиции 2 равен app2.

LaTeX

$$$\\text{(homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, ⋯⟩ = app₂}$$$

Lean4

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

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