hom_heq_of_cons_eq_cons — Mathlib

English

If p.cons e = p'.cons e' then the arrows e and e' are isomorphic, i.e., e ≍ e'.

Русский

Если p.cons e = p'.cons e', то стрелы e и e' изоморфны: e ≍ e'.

LaTeX

$$$\\forall p:\\, \\mathrm{Path}(a,b),\\; p'.\\mathrm{Path}(a,c),\\; e:\\, b\\to d,\\ e': c\\to d:\\; p.\\mathrm{cons}(e) = p'.\\mathrm{cons}(e') \\Rightarrow e \\simeq e'.$$$

Lean4

theorem hom_heq_of_cons_eq_cons {p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') :
    e ≍ e' := by injection h

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