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