def negEquiv : ℤ ≃ ℤ

Equations

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

def succEquiv : ℤ ≃ ℤ

Equations

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

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

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 swap_equiv {α : Type u_1} : (Fin 2 → α) ≃ (Fin 2 → α)

Equations

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