renameEquiv_symm — Mathlib

English

The inverse of a renameEquiv is the renameEquiv with the inverse bijection: (renameEquiv R f).symm = renameEquiv R f.symm.

Русский

Обратное к renameEquiv равно renameEquiv с обратной биекция: (renameEquiv R f).symm = renameEquiv R f.symm.

LaTeX

$$$(\\text{renameEquiv } R f).\\text{symm} = \\text{renameEquiv } R f^{\\mathrm{symm}}.$$$

Lean4

@[simp]
theorem renameEquiv_symm (f : σ ≃ τ) : (renameEquiv R f).symm = renameEquiv R f.symm :=
  rfl

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