eq_cast_iff_heq — Mathlib

English

Equivalence between equality after casting a path and heterogeneous equality of paths.

Русский

Эквивалентность между равенством после приведения пути и неоднородным равенством путей.

LaTeX

$$$ p' = p^{cast}_{hu hv} \\iff p' \\stackrel{HEQ}{\\sim} p $$$

Lean4

theorem eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) (p' : Path u' v') :
    p' = p.cast hu hv ↔ p' ≍ p :=
  ⟨fun h => ((p.cast_eq_iff_heq hu hv p').1 h.symm).symm, fun h => ((p.cast_eq_iff_heq hu hv p').2 h.symm).symm⟩

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