Equivs

def negEquiv : ℤ ≃ ℤ

Negation as an equivalence ℤ ≃ ℤ.

Equations

• negEquiv = { toFun := fun (n : ℤ) => -n, invFun := fun (n : ℤ) => -n, left_inv := negEquiv._proof_1, right_inv := negEquiv._proof_1 }

def succEquiv : ℤ ≃ ℤ

The successor map as an equivalence ℤ ≃ ℤ.

Equations

• succEquiv = { toFun := fun (n : ℤ) => n.succ, invFun := fun (n : ℤ) => n.pred, left_inv := Int.pred_succ, right_inv := Int.succ_pred }

def swap {α : Type u_1} : (Fin 2 → α) → Fin 2 → α

Swaps the two entries of a length-2 vector.

Equations

• swap x = ![x 1, x 0]

@[simp]

theorem swap_apply {α : Type u_1} (b : Fin 2 → α) : swap b = ![b 1, b 0]

theorem swap_involutive {α : Type u_1} (b : Fin 2 → α) : swap (swap b) = b

def swapEquiv {α : Type u_1} : (Fin 2 → α) ≃ (Fin 2 → α)

Swapping the two entries of a length-2 vector as an equivalence.

Equations

• swapEquiv = { toFun := swap, invFun := swap, left_inv := ⋯, right_inv := ⋯ }