ext₂ — Mathlib

English

If two morphisms φ, φ' in ComposableArrows C 2 agree on the three components app' at 0,1,2, then φ = φ'.

Русский

Если две стрелы φ, φ' между f и g в ComposableArrows C 2 совпадают на трёх компонентах на позициях 0,1,2, то они равны.

LaTeX

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

Lean4

theorem ext₂ {f g : ComposableArrows C 2} (h₀ : f.obj' 0 = g.obj' 0) (h₁ : f.obj' 1 = g.obj' 1)
    (h₂ : f.obj' 2 = g.obj' 2) (w₀ : f.map' 0 1 = eqToHom h₀ ≫ g.map' 0 1 ≫ eqToHom h₁.symm)
    (w₁ : f.map' 1 2 = eqToHom h₁ ≫ g.map' 1 2 ≫ eqToHom h₂.symm) : f = g :=
  ext_succ h₀ (ext₁ h₁ h₂ w₁) w₀

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