data.equiv.fin

# Equivalences for fin n#

def fin_zero_equiv  :

Equivalence between fin 0 and empty.

Equations
def fin_zero_equiv'  :

Equivalence between fin 0 and pempty.

Equations

Equivalence between fin 1 and unit.

Equations

Equivalence between fin 2 and bool.

Equations
def fin_congr {n m : } (h : n = m) :
fin n fin m

The 'identity' equivalence between fin n and fin m when n = m.

Equations
@[simp]
theorem fin_congr_apply_mk {n m : } (h : n = m) (k : ) (w : k < n) :
(fin_congr h) k, w⟩ = k, _⟩
@[simp]
theorem fin_congr_symm {n m : } (h : n = m) :
@[simp]
theorem fin_congr_apply_coe {n m : } (h : n = m) (k : fin n) :
theorem fin_congr_symm_apply_coe {n m : } (h : n = m) (k : fin m) :
def fin_succ_equiv' {n : } (i : fin n) :
fin (n + 1) option (fin n)

An equivalence that removes i and maps it to none. This is a version of fin.pred_above that produces option (fin n) instead of mapping both i.cast_succ and i.succ to i.

Equations
@[simp]
theorem fin_succ_equiv'_at {n : } (i : fin (n + 1)) :
theorem fin_succ_equiv'_below {n : } {i m : fin (n + 1)} (h : m < i) :
theorem fin_succ_equiv'_above {n : } {i m : fin (n + 1)} (h : i m) :
@[simp]
theorem fin_succ_equiv'_symm_none {n : } (i : fin (n + 1)) :
theorem fin_succ_equiv_symm'_some_below {n : } {i m : fin (n + 1)} (h : m < i) :
theorem fin_succ_equiv_symm'_some_above {n : } {i m : fin (n + 1)} (h : i m) :
theorem fin_succ_equiv_symm'_coe_below {n : } {i m : fin (n + 1)} (h : m < i) :
theorem fin_succ_equiv_symm'_coe_above {n : } {i m : fin (n + 1)} (h : i m) :
def fin_succ_equiv (n : ) :
fin (n + 1) option (fin n)

Equivalence between fin (n + 1) and option (fin n). This is a version of fin.pred that produces option (fin n) instead of requiring a proof that the input is not 0.

Equations
@[simp]
theorem fin_succ_equiv_zero {n : } :
@[simp]
theorem fin_succ_equiv_succ {n : } (m : fin n) :
@[simp]
@[simp]
theorem fin_succ_equiv_symm_some {n : } (m : fin n) :
@[simp]
theorem fin_succ_equiv_symm_coe {n : } (m : fin n) :
theorem fin_succ_equiv'_zero {n : } :

The equiv version of fin.pred_above_zero.

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

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

Equations
@[simp]
theorem fin_sum_fin_equiv_apply_left {m n : } (x : fin m) :
= x.val, _⟩
@[simp]
theorem fin_sum_fin_equiv_apply_right {m n : } (x : fin n) :
= m + x.val, _⟩
@[simp]
theorem fin_sum_fin_equiv_symm_apply_left {m n : } (x : fin (m + n)) (h : x < m) :
= sum.inl x.val, h⟩
@[simp]
theorem fin_sum_fin_equiv_symm_apply_right {m n : } (x : fin (m + n)) (h : m x) :
= sum.inr x.val - m, _⟩
def fin_add_flip {m n : } :
fin (m + n) fin (n + m)

The equivalence between fin (m + n) and fin (n + m) which rotates by n.

Equations
@[simp]
theorem fin_add_flip_apply_left {m n k : } (h : k < m) (hk : k < m + n := _) (hnk : n + k < n + m := _) :
fin_add_flip k, hk⟩ = n + k, hnk⟩
@[simp]
theorem fin_add_flip_apply_right {m n k : } (h₁ : m k) (h₂ : k < m + n) :
fin_add_flip k, h₂⟩ = k - m, _⟩
def fin_rotate (n : ) :

Rotate fin n one step to the right.

Equations
theorem fin_rotate_of_lt {n k : } (h : k < n) :
(fin_rotate (n + 1)) k, _⟩ = k + 1, _⟩
theorem fin_rotate_last' {n : } :
(fin_rotate (n + 1)) n, _⟩ = 0, _⟩
theorem fin_rotate_last {n : } :
(fin_rotate (n + 1)) (fin.last n) = 0
theorem fin.snoc_eq_cons_rotate {n : } {α : Type u_1} (v : fin n → α) (a : α) :
a = λ (i : fin (n + 1)), v ((fin_rotate (n + 1)) i)
@[simp]
theorem fin_rotate_zero  :
@[simp]
theorem fin_rotate_one  :
@[simp]
theorem fin_rotate_succ_apply {n : } (i : fin n.succ) :
(fin_rotate n.succ) i = i + 1
@[simp]
theorem fin_rotate_apply_zero {n : } :
theorem coe_fin_rotate_of_ne_last {n : } {i : fin n.succ} (h : i ) :
theorem coe_fin_rotate {n : } (i : fin n.succ) :
((fin_rotate n.succ) i) = ite (i = fin.last n) 0 (i + 1)
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
@[simp]
theorem fin.cast_le_order_iso_apply {n m : } (h : n m) (i : fin n) :
= (fin.cast_le h) i, _⟩
def fin.cast_le_order_iso {n m : } (h : n m) :
fin n ≃o {i // i < n}

Promote a fin n into a larger fin m, as a subtype where the underlying values are retained. This is the order_iso version of fin.cast_le.

Equations
@[simp]
theorem fin.cast_le_order_iso_symm_apply {n m : } (h : n m) (i : {i // i < n}) :
= i, _⟩
@[instance]

fin 0 is a subsingleton.

@[instance]

fin 1 is a subsingleton.