extendDomain_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem extendDomain_inv : (e.extendDomain f)⁻¹ = e⁻¹.extendDomain f :=
  rfl

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