swap — Mathlib

English

There exists an equivalence on WalkingPair that interchanges its two objects left and right; applying it twice yields the identity.

Русский

Существует эквивалентность на WalkingPair, которая меняет местами два объекта: левый и правый; дважды применённая перестановка даёт тождество.

LaTeX

$$$$ \exists S: WalkingPair \simeq WalkingPair,\ S(left)=right,\ S(right)=left,\ S\circ S=\mathrm{id}_{WalkingPair}. $$$$

Lean4

/-- The equivalence swapping left and right.
-/
def swap : WalkingPair ≃ WalkingPair
    where
  toFun
    | left => right
    | right => left
  invFun
    | left => right
    | right => left
  left_inv j := by cases j <;> rfl
  right_inv j := by cases j <;> rfl

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