hom_ext₃ — Mathlib

English

Two morphisms φ, φ' in ComposableArrows C 3 are equal if their 0,1,2 components agree.

Русский

Два морфизма φ, φ' в ComposableArrows C 3 равны, если их компоненты 0,1,2 совпадают.

LaTeX

$$$\\forall {f,g}, {\\phi,\\phi'}:\\, f \\to g,\n (\\text{app}' \\phi 0 = \\text{app}' \\phi' 0) \land (\\text{app}' \\phi 1 = \\text{app}' \\phi' 1) \land (\\text{app}' \\phi 2 = \\text{app}' \\phi' 2) \\Rightarrow \\phi = \\phi'.$$$

Lean4

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

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