cast_eq_iff_heq — Mathlib

English

For paths p and p' with endpoints related by hu,hv, casting p along hu hv equals p' if and only if p and p' are heterogeneously equal.

Русский

Для путей p и p' с концами, связанными tождествами hu, hv, cast-путь p вдоль hu hv равен p' тогда и только если p и p' являются неоднородно равными.

LaTeX

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

Lean4

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

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