extendDomain_symm — Mathlib

English

The inverse of an extended permutation equals the extension of the inverse: (e.extendDomain f)^{-1} = Perm.extendDomain e^{-1} f.

Русский

Обратное к расширенной перестановке равно расширению обратной: (e.extendDomain f)^{-1} = Perm.extendDomain e^{-1} f.

LaTeX

$$$(e.extendDomain f)^{\\;}{-1} = \\mathrm{Perm}.extendDomain\\ e^{ -1 } f$$$

Lean4

@[simp]
theorem extendDomain_symm : (e.extendDomain f).symm = Perm.extendDomain e.symm f :=
  rfl

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