cast_trans — Mathlib

English

The composition of two casts corresponds to the cast along the transitive composition: (cast h).trans (cast h') = cast (h.trans h').

Русский

Сложение двух преобразований cast соответствует преобразованию вдоль композиции индексов: (cast h).trans (cast h') = cast (h.trans h').

LaTeX

$$(cast_R M h).trans (cast_R M h') = cast_R M (h.trans h')$$

Lean4

@[simp]
theorem cast_trans {i j k} (h : i = j) (h' : j = k) : (cast R M h).trans (cast R M h') = cast R M (h.trans h') :=
  reindex_trans _ _

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