selfApplyEquiv — Mathlib

English

The map x ↦ x ◃ x is a bijection with inverse x ↦ x ◃⁻¹ x.

Русский

Отображение x ↦ x ◃ x является биекция с обратным отображением x ↦ x ◃⁻¹ x.

LaTeX

$$$\exists e: R \simeq R,\forall x: R, e(x) = x \triangleleft x \land e^{-1}(x) = x \triangleleft^{-1} x$$$

Lean4

/-- The map `x ↦ x ◃ x` is a bijection.  (This has applications for the
regular isotopy version of the Reidemeister I move for knot diagrams.)
-/
def selfApplyEquiv (R : Type*) [Rack R] : R ≃ R where
  toFun x := x ◃ x
  invFun x := x ◃⁻¹ x
  left_inv x := by simp
  right_inv x := by simp

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