mathlib documentation

data.equiv.fin

Equivalences for fin n

Equivalence between fin 0 and empty.

Equations

Equivalence between fin 0 and pempty.

Equations

Equivalence between fin 1 and punit.

Equations

Equivalence between fin 2 and bool.

Equations
def fin_succ_equiv (n : ) :

Equivalence between fin n.succ and option (fin n)

Equations
@[simp]

@[simp]
theorem fin_succ_equiv_succ {n : } (m : fin n) :

@[simp]

@[simp]
theorem fin_succ_equiv_symm_some {n : } (m : fin n) :

def sum_fin_sum_equiv {m n : } :
fin m fin n fin (m + n)

Equivalence between fin m ⊕ fin n and fin (m + n)

Equations
def fin_prod_fin_equiv {m n : } :
fin m × fin n fin (m * n)

Equivalence between fin m × fin n and fin (m * n)

Equations
@[instance]

fin 0 is a subsingleton.

@[instance]

fin 1 is a subsingleton.