cast_trans — Mathlib

English

The transitive cast composition equals the cast of composed equality; (cast h).trans (cast h2) = cast (h.trans h2).

Русский

Составление приведения через транспозицию равно приведению от композиции равенств.

LaTeX

$$$(\\mathrm{cast}(h)).trans(\\mathrm{cast}(h2)) = \\mathrm{cast}(h\\trans h2).$$$

Lean4

@[simp]
theorem cast_trans {α β γ} (h : α = β) (h2 : β = γ) : (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (h.trans h2) :=
  ext fun x => by substs h h2; rfl

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