eq_cast_iff_heq — Mathlib

English

For Path objects p from u to v and p' from u' to v', with hu: u = u' and hv: v = v', the equality p.cast hu hv = p' is equivalent to p and p' being heterogeneously equal.

Русский

Для путей p: u → v и p': u' → v', при hu: u = u' и hv: v = v', равенство p.cast hu hv = p' эквивалентно тому, что p и p' относятся к друг другу как неоднородно равные.

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') (e : u ⟶ v) (e' : u' ⟶ v') :
    e' = e.cast hu hv ↔ e' ≍ e := by
  rw [eq_comm, Hom.cast_eq_iff_heq]
  exact ⟨HEq.symm, HEq.symm⟩

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