act' — Mathlib

English

For a rack R, each element x induces a permutation act'(x) of R, given by y ↦ x ◃ y, with inverse invAct(x) given by y ↦ x ◃⁻¹ y.

Русский

Для рака R каждое x порождает перестановку act'(x) на R, задаваемую y ↦ x ◃ y, а обратное действие invAct(x) — y ↦ x ◃⁻¹ y.

LaTeX

$$$act'(x) : R \to R\quad\text{with inverse}\quad invAct(x) : R \to R$$$

Lean4

/-- A rack acts on itself by equivalences. -/
def act' (x : R) : R ≃ R where
  toFun := Shelf.act x
  invFun := invAct x
  left_inv := left_inv x
  right_inv := right_inv x

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