mathlib documentation

data.equiv.fin

Equivalences for `fin n` #

def fin_zero_equiv :

fin 0 ≃ empty

Equivalence between fin 0 and empty.

Equations

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

def fin_zero_equiv' :

fin 0 ≃ pempty

Equivalence between fin 0 and pempty.

Equations

fin_zero_equiv' = equiv.equiv_pempty fin_zero_equiv'._proof_1

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}

def fin_two_equiv :

Equivalence between fin 2 and bool.

Equations

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

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

fin_congr h = equiv.subtype_equiv_right _

@[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) :

(fin_congr h).symm = fin_congr _

@[simp]

theorem fin_congr_apply_coe {n m : ℕ} (h : n = m) (k : fin n) :

↑(⇑(fin_congr h) k) = ↑k

theorem fin_congr_symm_apply_coe {n m : ℕ} (h : n = m) (k : fin m) :

↑(⇑((fin_congr h).symm) k) = ↑k

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

fin_succ_equiv' i = {to_fun := λ (x : fin (n + 1)), ite (x = ⇑fin.cast_succ i) none (some (i.pred_above x)), inv_fun := λ (x : option (fin n)), x.cases_on' (⇑fin.cast_succ i) ⇑((⇑fin.cast_succ i).succ_above), left_inv := _, right_inv := _}

@[simp]

theorem fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :

⇑(fin_succ_equiv' i) (⇑fin.cast_succ i) = none

theorem fin_succ_equiv'_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :

⇑(fin_succ_equiv' i) (⇑fin.cast_succ m) = some m

theorem fin_succ_equiv'_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :

⇑(fin_succ_equiv' i) m.succ = some m

@[simp]

theorem fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :

⇑((fin_succ_equiv' i).symm) none = ⇑fin.cast_succ i

theorem fin_succ_equiv_symm'_some_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :

⇑((fin_succ_equiv' i).symm) (some m) = ⇑fin.cast_succ m

theorem fin_succ_equiv_symm'_some_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :

⇑((fin_succ_equiv' i).symm) (some m) = m.succ

theorem fin_succ_equiv_symm'_coe_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :

⇑((fin_succ_equiv' i).symm) ↑m = ⇑fin.cast_succ m

theorem fin_succ_equiv_symm'_coe_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :

⇑((fin_succ_equiv' i).symm) ↑m = m.succ

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

fin_succ_equiv n = n.cases_on {to_fun := λ (_x : fin (0 + 1)), none, inv_fun := λ (_x : option (fin 0)), 0, left_inv := fin_succ_equiv._proof_1, right_inv := fin_succ_equiv._proof_2} (λ (_x : ℕ), fin_succ_equiv' 0)

@[simp]

theorem fin_succ_equiv_zero {n : ℕ} :

⇑(fin_succ_equiv n) 0 = none

@[simp]

theorem fin_succ_equiv_succ {n : ℕ} (m : fin n) :

⇑(fin_succ_equiv n) m.succ = some m

@[simp]

theorem fin_succ_equiv_symm_none {n : ℕ} :

⇑((fin_succ_equiv n).symm) none = 0

@[simp]

theorem fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :

⇑((fin_succ_equiv n).symm) (some m) = m.succ

@[simp]

theorem fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :

⇑((fin_succ_equiv n).symm) ↑m = m.succ

theorem fin_succ_equiv'_zero {n : ℕ} :

fin_succ_equiv' 0 = fin_succ_equiv (n + 1)

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

fin_sum_fin_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 := _}

@[simp]

theorem fin_sum_fin_equiv_apply_left {m n : ℕ} (x : fin m) :

⇑fin_sum_fin_equiv (sum.inl x) = ⟨x.val, _⟩

@[simp]

theorem fin_sum_fin_equiv_apply_right {m n : ℕ} (x : fin n) :

⇑fin_sum_fin_equiv (sum.inr x) = ⟨m + x.val, _⟩

@[simp]

theorem fin_sum_fin_equiv_symm_apply_left {m n : ℕ} (x : fin (m + n)) (h : ↑x < m) :

⇑(fin_sum_fin_equiv.symm) x = sum.inl ⟨x.val, h⟩

@[simp]

theorem fin_sum_fin_equiv_symm_apply_right {m n : ℕ} (x : fin (m + n)) (h : m ≤ ↑x) :

⇑(fin_sum_fin_equiv.symm) 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

fin_add_flip = (fin_sum_fin_equiv.symm.trans (equiv.sum_comm (fin m) (fin n))).trans fin_sum_fin_equiv

@[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 : ℕ) :

equiv.perm (fin n)

Rotate fin n one step to the right.

Equations

fin_rotate (n + 1) = fin_add_flip.trans (fin_congr _)
fin_rotate 0 = equiv.refl (fin 0)

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 : α) :

fin.snoc v a = λ (i : fin (n + 1)), fin.cons a v (⇑(fin_rotate (n + 1)) i)

@[simp]

theorem fin_rotate_zero :

fin_rotate 0 = equiv.refl (fin 0)

@[simp]

theorem fin_rotate_one :

fin_rotate 1 = equiv.refl (fin 1)

@[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 : ℕ} :

⇑(fin_rotate n.succ) 0 = 1

theorem coe_fin_rotate_of_ne_last {n : ℕ} {i : fin n.succ} (h : i ≠ fin.last n) :

↑(⇑(fin_rotate n.succ) i) = ↑i + 1

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

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 := _}

@[protected, instance]

def subsingleton_fin_zero :

subsingleton (fin 0)

fin 0 is a subsingleton.

@[protected, instance]

def subsingleton_fin_one :

subsingleton (fin 1)

fin 1 is a subsingleton.