cast_heq — Mathlib

English

Casting a path along equal endpoints yields a heterogeneous-equal path to the original one.

Русский

Приведение пути по равным концам даёт путь, гомологичный по неоднородному равенству к исходному путю.

LaTeX

$$$ p^{cast}_{hu hv} \\;\\stackrel{HEQ}{\\sim}\\; p $$$

Lean4

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

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