obj_ext — Mathlib

English

Two CostructuredArrow objects x,y are equal if their left components are equal and the right components satisfy the compatibility S.map (eqToHom hl) ≫ y.hom = x.hom.

Русский

Два объекта CostructuredArrow x, y равны, если их левые компоненты равны и выполняется совместимость S.map (eqToHom hl) ≫ y.hom = x.hom.

LaTeX

$$$x.left = y.left \\land S.map (eqToHom (\\text{hl})) \\;\\gg\\; y.hom = x.hom \\Rightarrow x = y$$$

Lean4

theorem obj_ext (x y : CostructuredArrow S T) (hl : x.left = y.left) (hh : S.map (eqToHom hl) ≫ y.hom = x.hom) :
    x = y := by
  cases x
  cases y
  cases hl
  cat_disch

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