Equivalences for `fin n`

source

def fin_zero_equiv :

fin 0 ≃ empty

Equivalence between fin 0 and empty.

Equations

fin_zero_equiv = {to_fun := fin_zero_elim (λ (a : fin 0), empty), inv_fun := empty.elim (fin 0), left_inv := fin_zero_equiv._proof_1, right_inv := fin_zero_equiv._proof_2}

source

def fin_zero_equiv' :

fin 0 ≃ pempty

Equivalence between fin 0 and pempty.

Equations

fin_zero_equiv' = equiv.equiv_pempty fin.elim0

source

def fin_one_equiv :

fin 1 ≃ punit

Equivalence between fin 1 and punit.

Equations

fin_one_equiv = {to_fun := λ (_x : fin 1), (), inv_fun := λ (_x : punit), 0, left_inv := fin_one_equiv._proof_1, right_inv := fin_one_equiv._proof_2}

source

def fin_two_equiv :

fin 2 ≃ bool

Equivalence between fin 2 and bool.

Equations

fin_two_equiv = {to_fun := fin.cases bool.ff (λ (_x : fin 1), bool.tt), inv_fun := λ (b : bool), cond b 1 0, left_inv := fin_two_equiv._proof_1, right_inv := fin_two_equiv._proof_2}

source

def fin_succ_equiv (n : ℕ) :

fin n.succ ≃ option (fin n)

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

Equations

fin_succ_equiv n = {to_fun := λ (x : fin n.succ), fin.cases option.none option.some x, inv_fun := λ (x : option (fin n)), x.rec_on 0 fin.succ, left_inv := _, right_inv := _}

source

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

sum_fin_sum_equiv = {to_fun := λ (x : fin m ⊕ fin n), x.rec_on (λ (y : fin m), ⟨y.val, _⟩) (λ (y : fin n), ⟨m + y.val, _⟩), inv_fun := λ (x : fin (m + n)), dite (x.val < m) (λ (H : x.val < m), sum.inl ⟨x.val, H⟩) (λ (H : ¬x.val < m), sum.inr ⟨x.val - m, _⟩), left_inv := _, right_inv := _}

source

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

fin_prod_fin_equiv = {to_fun := λ (x : fin m × fin n), ⟨x.snd.val + n * x.fst.val, _⟩, inv_fun := λ (x : fin (m * n)), have H : 0 < n, from _, (⟨x.val / n, _⟩, ⟨x.val % n, _⟩), left_inv := _, right_inv := _}

source

@[instance]

def subsingleton_fin_zero :

subsingleton (fin 0)

fin 0 is a subsingleton.

Equations

subsingleton_fin_zero = _

source

@[instance]

def subsingleton_fin_one :

subsingleton (fin 1)

fin 1 is a subsingleton.

Equations

subsingleton_fin_one = _

mathlib documentation

data.equiv.fin

Equivalences for `fin n`

General documentation

Additional documentation

Library

mathlib documentation

data.​equiv.​fin

Equivalences for fin n

General documentation

Additional documentation

Library

data.equiv.fin

Equivalences for `fin n`