toPerm — Mathlib

English

From an involutive function f, construct a permutation whose forward and inverse maps are f.

Русский

Из инволютивной функции f строится перестановка с прямым и обратным отображением, равными f.

LaTeX

$$toPerm(f,h) is the permutation with toFun = f and invFun = f$$

Lean4

/-- Convert an involutive function `f` to a permutation with `toFun = invFun = f`. -/
def toPerm (f : α → α) (h : Involutive f) : Equiv.Perm α :=
  ⟨f, f, h.leftInverse, h.rightInverse⟩

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