cast_eq_iff_heq — Mathlib

English

Let u,v,u',v' be objects of a universe U, and hu: u = u' and hv: v = v'. For arrows e: u → v and e': u' → v', the equality e' = e cast along hu hv is equivalent to e and e' being heterogeneous-equal.

Русский

Пусть u,v,u',v' — объекты множества U, hu: u = u' и hv: v = v'. Для стрел e: u → v и e': u' → v' равенство e' = e.cast hu hv эквивалентно тому, что e и e' несоотносятся по неоднородному равенству (HEQ).

LaTeX

$$$ e' = e^{\\mathrm{cast}}_{hu hv} \\iff e \\;\\stackrel{HEQ}{\\sim}\\; e', $$$

Lean4

theorem cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v') :
    e.cast hu hv = e' ↔ e ≍ e' := by
  rw [Hom.cast_eq_cast]
  exact _root_.cast_eq_iff_heq

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