obj_eq_of_cons_eq_cons — Mathlib

English

If p.cons e = p'.cons e' for some paths p, p' and edges e, e', then the endpoints of p and p' coincide, i.e., b = c.

Русский

Если p.cons e = p'.cons e' для некоторых путей p, p' и ребер e, e', то концы путей совпадают: b = c.

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 b=c.$$$

Lean4

theorem obj_eq_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') :
    b = c := by injection h

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