homOfEq_injective — Mathlib

English

If an equality of transported arrows holds, then the original arrows are heterogeneously equal (HEq).

Русский

Если верно равенство перенесённых стрел, то исходные стрелы равны гетерогенно (HEq).

LaTeX

$$f ≍ f' (HEq)$$

Lean4

theorem homOfEq_injective {X X' Y Y' : V} (hX : X = X') (hY : Y = Y') {f g : X ⟶ Y}
    (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g :=
  by
  subst hX hY
  exact h

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