cast_eq_of_cons_eq_cons — Mathlib

English

If two paths p and p' become equal after appending the same arrow e (from v to w) and e' (from v' to w), then the cast of p along the induced equality equals p'.

Русский

Если два пути p и p' становятся равными после добавления одного и того же ребра e: v→w и e': v'→w, тогда приведённый путь p вдоль соответствующего тождества равен p'.

LaTeX

$$$ h: p.concat\\; e = p'.concat\\; e' \\Rightarrow p.cast rfl (obj\\_eq\\_of\\_cons\\_eq\\_cons h) = p' $$$

Lean4

theorem cast_eq_of_cons_eq_cons {u v v' w : U} {p : Path u v} {p' : Path u v'} {e : v ⟶ w} {e' : v' ⟶ w}
    (h : p.cons e = p'.cons e') : p.cast rfl (obj_eq_of_cons_eq_cons h) = p' :=
  by
  rw [Path.cast_eq_iff_heq]
  exact heq_of_cons_eq_cons h

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