cast_eq_cast — Mathlib

English

Transport along an equality is the same as casting using the corresponding equality to a concrete cast.

Русский

Перенос вдоль равенства эквивалентен приведения к конкретному отображению через эквивалентность.

LaTeX

$$$c.\\mathrm{cast}\\;hmn = \\mathrm{cast}(hmn \\;\\mathrm{▸}\\; \\mathrm{rfl})\,c.$$$

Lean4

theorem cast_eq_cast (c : Composition m) (hmn : m = n) : c.cast hmn = cast (hmn ▸ rfl) c :=
  by
  subst m
  rfl

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