renameEquiv_trans — Mathlib

English

For bijections e: σ ≃ τ and f: τ ≃ α, the transitive composition of renameEquiv is the renameEquiv of the composed bijection: (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f).

Русский

Для биекций e: σ ≃ τ и f: τ ≃ α, составление renameEquiv влечет renameEquiv для композиции: (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f).

LaTeX

$$$(\\text{renameEquiv } R e).\\text{trans} (\\text{renameEquiv } R f) = \\text{renameEquiv } R (e.\\text{trans } f).$$$

Lean4

@[simp]
theorem renameEquiv_trans (e : σ ≃ τ) (f : τ ≃ α) :
    (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f) :=
  AlgEquiv.ext (rename_rename e f)

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