cast_cast — Mathlib

English

Casting first by h and then by h' is the same as casting by h followed by h' together, i.e., Sym.cast h' (Sym.cast h s) = Sym.cast (h.trans h') s.

Русский

Сложение приводдений совпадает: последовательное приведение по h и затем по h' эквивалентно приведениям по композиции h ∘ h'.

LaTeX

$$$\\mathrm{Sym.cast}\\, h'\\, (\\mathrm{Sym.cast}\\, h\\, s) = \\mathrm{Sym.cast}\\, (h \\trans h')\\, s$$$

Lean4

@[simp]
theorem cast_cast {n'' : ℕ} (h : n = n') (h' : n' = n'') : Sym.cast h' (Sym.cast h s) = Sym.cast (h.trans h') s :=
  rfl

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