hom_cast_eq_of_cons_eq_cons — Mathlib

English

If two paths p and p' are equal after appending arrows e and e' to their ends, then the corresponding casted arrows are equal.

Русский

Если два пути p и p' равны после добавления концов e и e' к их концам, то соответствующие приведённые стрелы равны.

LaTeX

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

Lean4

theorem hom_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') : e.cast (obj_eq_of_cons_eq_cons h) rfl = e' :=
  by
  rw [Hom.cast_eq_iff_heq]
  exact hom_heq_of_cons_eq_cons h

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