mathlib3 documentation

logic.equiv.fin

Equivalences for fin n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def fin_zero_equiv  :
fin 0 ≃ empty

Equivalence between fin 0 and empty.

Equations
source
def fin_zero_equiv'  :
fin 0 ≃ pempty

Equivalence between fin 0 and pempty.

Equations
source
def fin_one_equiv  :
fin 1 ≃ unit

Equivalence between fin 1 and unit.

Equations
source
def fin_two_equiv  :
fin 2 ≃ bool

Equivalence between fin 2 and bool.

Equations
source
@[simp]
theorem pi_fin_two_equiv_symm_apply (α : fin 2 → Type u) :
⇑((pi_fin_two_equiv α).symm) = λ (p : α 0 × α 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
source
def pi_fin_two_equiv (α : fin 2 → Type u) :
(Π (i : fin 2), α i) ≃ α 0 × α 1

Π i : fin 2, α i is equivalent to α 0 × α 1. See also fin_two_arrow_equiv for a non-dependent version and prod_equiv_pi_fin_two for a version with inputs α β : Type u.

Equations
source
@[simp]
theorem pi_fin_two_equiv_apply (α : fin 2 → Type u) :
⇑(pi_fin_two_equiv α) = λ (f : Π (i : fin 2), α i), (f 0, f 1)
source
theorem fin.preimage_apply_01_prod {α : fin 2 → Type u} (s : set (α 0)) (t : set (α 1)) :
(λ (f : Π (i : fin 2), α i), (f 0, f 1)) ⁻¹' s ×ˢ t = set.univ.pi (fin.cons s (fin.cons t fin.elim0))
source
theorem fin.preimage_apply_01_prod' {α : Type u} (s t : set α) :
(λ (f : fin 2 → α), (f 0, f 1)) ⁻¹' s ×ˢ t = set.univ.pi ![s, t]
source
def prod_equiv_pi_fin_two (α β : Type u) :
α × β ≃ Π (i : fin 2), ![α, β] i

A product space α × β is equivalent to the space Π i : fin 2, γ i, where γ = fin.cons α (fin.cons β fin_zero_elim). See also pi_fin_two_equiv and fin_two_arrow_equiv.

Equations
source
@[simp]
theorem prod_equiv_pi_fin_two_apply (α β : Type u) :
⇑(prod_equiv_pi_fin_two α β) = λ (p : fin.cons α (fin.cons β fin_zero_elim) 0 × fin.cons α (fin.cons β fin_zero_elim) 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
source
@[simp]
theorem prod_equiv_pi_fin_two_symm_apply (α β : Type u) :
⇑((prod_equiv_pi_fin_two α β).symm) = λ (f : Π (i : fin 2), fin.cons α (fin.cons β fin_zero_elim) i), (f 0, f 1)
source
@[simp]
theorem fin_two_arrow_equiv_apply (α : Type u_1) :
⇑(fin_two_arrow_equiv α) = (pi_fin_two_equiv (λ (_x : fin 2), α)).to_fun
source
def fin_two_arrow_equiv (α : Type u_1) :
(fin 2 → α) ≃ α × α

The space of functions fin 2 → α is equivalent to α × α. See also pi_fin_two_equiv and prod_equiv_pi_fin_two.

Equations
source
@[simp]
theorem fin_two_arrow_equiv_symm_apply (α : Type u_1) :
⇑((fin_two_arrow_equiv α).symm) = λ (x : α × α), ![x.fst, x.snd]
source
def order_iso.pi_fin_two_iso (α : fin 2 → Type u) [Π (i : fin 2), preorder (α i)] :
(Π (i : fin 2), α i) ≃o α 0 × α 1

Π i : fin 2, α i is order equivalent to α 0 × α 1. See also order_iso.fin_two_arrow_equiv for a non-dependent version.

Equations
source
def order_iso.fin_two_arrow_iso (α : Type u_1) [preorder α] :
(fin 2 → α) ≃o α × α

The space of functions fin 2 → α is order equivalent to α × α. See also order_iso.pi_fin_two_iso.

Equations
source
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
source
@[simp]
theorem fin_congr_apply_mk {n m : ℕ} (h : n = m) (k : ℕ) (w : k < n) :
⇑(fin_congr h) ⟨k, w⟩ = ⟨k, _⟩
source
@[simp]
theorem fin_congr_symm {n m : ℕ} (h : n = m) :
(fin_congr h).symm = fin_congr _
source
@[simp]
theorem fin_congr_apply_coe {n m : ℕ} (h : n = m) (k : fin n) :
↑(⇑(fin_congr h) k) = ↑k
source
theorem fin_congr_symm_apply_coe {n m : ℕ} (h : n = m) (k : fin m) :
↑(⇑((fin_congr h).symm) k) = ↑k
source
def fin_succ_equiv' {n : ℕ} (i : fin (n + 1)) :
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
source
@[simp]
theorem fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
⇑(fin_succ_equiv' i) i = option.none
source
@[simp]
theorem fin_succ_equiv'_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑(fin_succ_equiv' i) (⇑(i.succ_above) j) = option.some j
source
theorem fin_succ_equiv'_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : ⇑fin.cast_succ m < i) :
⇑(fin_succ_equiv' i) (⇑fin.cast_succ m) = option.some m
source
theorem fin_succ_equiv'_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ ⇑fin.cast_succ m) :
⇑(fin_succ_equiv' i) m.succ = option.some m
source
@[simp]
theorem fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
⇑((fin_succ_equiv' i).symm) option.none = i
source
@[simp]
theorem fin_succ_equiv'_symm_some {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑((fin_succ_equiv' i).symm) (option.some j) = ⇑(i.succ_above) j
source
theorem fin_succ_equiv'_symm_some_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : ⇑fin.cast_succ m < i) :
⇑((fin_succ_equiv' i).symm) (option.some m) = ⇑fin.cast_succ m
source
theorem fin_succ_equiv'_symm_some_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ ⇑fin.cast_succ m) :
⇑((fin_succ_equiv' i).symm) (option.some m) = m.succ
source
theorem fin_succ_equiv'_symm_coe_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : ⇑fin.cast_succ m < i) :
⇑((fin_succ_equiv' i).symm) ↑m = ⇑fin.cast_succ m
source
theorem fin_succ_equiv'_symm_coe_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ ⇑fin.cast_succ m) :
⇑((fin_succ_equiv' i).symm) ↑m = m.succ
source
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
source
@[simp]
theorem fin_succ_equiv_zero {n : ℕ} :
⇑(fin_succ_equiv n) 0 = option.none
source
@[simp]
theorem fin_succ_equiv_succ {n : ℕ} (m : fin n) :
⇑(fin_succ_equiv n) m.succ = option.some m
source
@[simp]
theorem fin_succ_equiv_symm_none {n : ℕ} :
⇑((fin_succ_equiv n).symm) option.none = 0
source
@[simp]
theorem fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :
⇑((fin_succ_equiv n).symm) (option.some m) = m.succ
source
@[simp]
theorem fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
⇑((fin_succ_equiv n).symm) ↑m = m.succ
source
theorem fin_succ_equiv'_zero {n : ℕ} :
fin_succ_equiv' 0 = fin_succ_equiv n

The equiv version of fin.pred_above_zero.

source
theorem fin_succ_equiv'_last_apply {n : ℕ} {i : fin (n + 1)} (h : i ≠ fin.last n) :
⇑(fin_succ_equiv' (fin.last n)) i = ↑(i.cast_lt _)
source
theorem fin_succ_equiv'_ne_last_apply {n : ℕ} {i j : fin (n + 1)} (hi : i ≠ fin.last n) (hj : j ≠ i) :
⇑(fin_succ_equiv' i) j = ↑((i.cast_lt _).pred_above j)
source
def fin_succ_above_equiv {n : ℕ} (p : fin (n + 1)) :
fin n ≃o {x // x ≠ p}

succ_above as an order isomorphism between fin n and {x : fin (n + 1) // x ≠ p}.

Equations
source
theorem fin_succ_above_equiv_apply {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑(fin_succ_above_equiv p) i = ⟨⇑(p.succ_above) i, _⟩
source
theorem fin_succ_above_equiv_symm_apply_last {n : ℕ} (x : {x // x ≠ fin.last n}) :
⇑((fin_succ_above_equiv (fin.last n)).symm) x = ↑x.cast_lt _
source
theorem fin_succ_above_equiv_symm_apply_ne_last {n : ℕ} {p : fin (n + 1)} (h : p ≠ fin.last n) (x : {x // x ≠ p}) :
⇑((fin_succ_above_equiv p).symm) x = (p.cast_lt _).pred_above ↑x
source
def fin_succ_equiv_last {n : ℕ} :
fin (n + 1) ≃ option (fin n)

equiv between fin (n + 1) and option (fin n) sending fin.last n to none

Equations
source
@[simp]
theorem fin_succ_equiv_last_cast_succ {n : ℕ} (i : fin n) :
⇑fin_succ_equiv_last (⇑fin.cast_succ i) = option.some i
source
@[simp]
theorem fin_succ_equiv_last_last {n : ℕ} :
⇑fin_succ_equiv_last (fin.last n) = option.none
source
@[simp]
theorem fin_succ_equiv_last_symm_some {n : ℕ} (i : fin n) :
⇑(fin_succ_equiv_last.symm) (option.some i) = ⇑fin.cast_succ i
source
@[simp]
theorem fin_succ_equiv_last_symm_coe {n : ℕ} (i : fin n) :
⇑(fin_succ_equiv_last.symm) ↑i = ⇑fin.cast_succ i
source
@[simp]
theorem fin_succ_equiv_last_symm_none {n : ℕ} :
⇑(fin_succ_equiv_last.symm) option.none = fin.last n
source
@[simp]
theorem equiv.pi_fin_succ_above_equiv_symm_apply {n : ℕ} (α : fin (n + 1) → Type u) (i : fin (n + 1)) :
⇑((equiv.pi_fin_succ_above_equiv α i).symm) = λ (f : α i × Π (j : fin n), α (⇑(i.succ_above) j)), i.insert_nth f.fst f.snd
source
def equiv.pi_fin_succ_above_equiv {n : ℕ} (α : fin (n + 1) → Type u) (i : fin (n + 1)) :
(Π (j : fin (n + 1)), α j) ≃ α i × Π (j : fin n), α (⇑(i.succ_above) j)

Equivalence between Π j : fin (n + 1), α j and α i × Π j : fin n, α (fin.succ_above i j).

Equations
source
@[simp]
theorem equiv.pi_fin_succ_above_equiv_apply {n : ℕ} (α : fin (n + 1) → Type u) (i : fin (n + 1)) :
⇑(equiv.pi_fin_succ_above_equiv α i) = λ (f : Π (j : fin (n + 1)), α j), (f i, λ (j : fin n), f (⇑(i.succ_above) j))
source
def order_iso.pi_fin_succ_above_iso {n : ℕ} (α : fin (n + 1) → Type u) [Π (i : fin (n + 1)), has_le (α i)] (i : fin (n + 1)) :
(Π (j : fin (n + 1)), α j) ≃o α i × Π (j : fin n), α (⇑(i.succ_above) j)

Order isomorphism between Π j : fin (n + 1), α j and α i × Π j : fin n, α (fin.succ_above i j).

Equations
source
def equiv.pi_fin_succ (n : ℕ) (β : Type u) :
(fin (n + 1) → β) ≃ β × (fin n → β)

Equivalence between fin (n + 1) → β and β × (fin n → β).

Equations
source
@[simp]
theorem equiv.pi_fin_succ_symm_apply (n : ℕ) (β : Type u) :
⇑((equiv.pi_fin_succ n β).symm) = λ (f : β × (fin n → β)), fin.cons f.fst f.snd
source
@[simp]
theorem equiv.pi_fin_succ_apply (n : ℕ) (β : Type u) :
⇑(equiv.pi_fin_succ n β) = λ (f : fin (n + 1) → β), (f 0, λ (j : fin n), f j.succ)
source
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
source
@[simp]
theorem fin_sum_fin_equiv_apply_left {m n : ℕ} (i : fin m) :
⇑fin_sum_fin_equiv (sum.inl i) = ⇑(fin.cast_add n) i
source
@[simp]
theorem fin_sum_fin_equiv_apply_right {m n : ℕ} (i : fin n) :
⇑fin_sum_fin_equiv (sum.inr i) = ⇑(fin.nat_add m) i
source
@[simp]
theorem fin_sum_fin_equiv_symm_apply_cast_add {m n : ℕ} (x : fin m) :
⇑(fin_sum_fin_equiv.symm) (⇑(fin.cast_add n) x) = sum.inl x
source
@[simp]
theorem fin_sum_fin_equiv_symm_apply_nat_add {m n : ℕ} (x : fin n) :
⇑(fin_sum_fin_equiv.symm) (⇑(fin.nat_add m) x) = sum.inr x
source
@[simp]
theorem fin_sum_fin_equiv_symm_last {n : ℕ} :
⇑(fin_sum_fin_equiv.symm) (fin.last n) = sum.inr 0
source
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
source
@[simp]
theorem fin_add_flip_apply_cast_add {m : ℕ} (k : fin m) (n : ℕ) :
⇑fin_add_flip (⇑(fin.cast_add n) k) = ⇑(fin.nat_add n) k
source
@[simp]
theorem fin_add_flip_apply_nat_add {n : ℕ} (k : fin n) (m : ℕ) :
⇑fin_add_flip (⇑(fin.nat_add m) k) = ⇑(fin.cast_add m) k
source
@[simp]
theorem fin_add_flip_apply_mk_left {m n k : ℕ} (h : k < m) (hk : k < m + n := _) (hnk : n + k < n + m := _) :
⇑fin_add_flip ⟨k, hk⟩ = ⟨n + k, hnk⟩
source
@[simp]
theorem fin_add_flip_apply_mk_right {m n k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
⇑fin_add_flip ⟨k, h₂⟩ = ⟨k - m, _⟩
source
def fin_rotate (n : ℕ) :
equiv.perm (fin n)

Rotate fin n one step to the right.

Equations
source
theorem fin_rotate_of_lt {n k : ℕ} (h : k < n) :
⇑(fin_rotate (n + 1)) ⟨k, _⟩ = ⟨k + 1, _⟩
source
theorem fin_rotate_last' {n : ℕ} :
⇑(fin_rotate (n + 1)) ⟨n, _⟩ = ⟨0, _⟩
source
theorem fin_rotate_last {n : ℕ} :
⇑(fin_rotate (n + 1)) (fin.last n) = 0
source
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)
source
@[simp]
theorem fin_rotate_zero  :
fin_rotate 0 = equiv.refl (fin 0)
source
@[simp]
theorem fin_rotate_one  :
fin_rotate 1 = equiv.refl (fin 1)
source
@[simp]
theorem fin_rotate_succ_apply {n : ℕ} (i : fin n.succ) :
⇑(fin_rotate n.succ) i = i + 1
source
@[simp]
theorem fin_rotate_apply_zero {n : ℕ} :
⇑(fin_rotate n.succ) 0 = 1
source
theorem coe_fin_rotate_of_ne_last {n : ℕ} {i : fin n.succ} (h : i ≠ fin.last n) :
↑(⇑(fin_rotate n.succ) i) = ↑i + 1
source
theorem coe_fin_rotate {n : ℕ} (i : fin n.succ) :
↑(⇑(fin_rotate n.succ) i) = ite (i = fin.last n) 0 (↑i + 1)
source
@[simp]
theorem fin_prod_fin_equiv_symm_apply {m n : ℕ} (x : fin (m * n)) :
⇑(fin_prod_fin_equiv.symm) x = (x.div_nat, x.mod_nat)
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
source
@[simp]
theorem fin_prod_fin_equiv_apply_val {m n : ℕ} (x : fin m × fin n) :
(⇑fin_prod_fin_equiv x).val = ↑(x.snd) + n * ↑(x.fst)
source
@[simp]
theorem nat.div_mod_equiv_apply (n : ℕ) [ne_zero n] (a : ℕ) :
⇑(n.div_mod_equiv) a = (a / n, ↑a)
source
def nat.div_mod_equiv (n : ℕ) [ne_zero n] :
ℕ ≃ ℕ × fin n

The equivalence induced by a ↦ (a / n, a % n) for nonzero n.

This is like fin_prod_fin_equiv.symm but with m infinite. See nat.div_mod_unique for a similar propositional statement.

Equations
source
@[simp]
theorem nat.div_mod_equiv_symm_apply (n : ℕ) [ne_zero n] (p : ℕ × fin n) :
⇑(n.div_mod_equiv.symm) p = p.fst * n + ↑(p.snd)
source
@[simp]
theorem int.div_mod_equiv_apply (n : ℕ) [ne_zero n] (a : ℤ) :
⇑(int.div_mod_equiv n) a = (a / ↑n, ↑(a.nat_mod ↑n))
source
def int.div_mod_equiv (n : ℕ) [ne_zero n] :
ℤ ≃ ℤ × fin n

The equivalence induced by a ↦ (a / n, a % n) for nonzero n.

See int.div_mod_unique for a similar propositional statement.

Equations
source
@[simp]
theorem int.div_mod_equiv_symm_apply (n : ℕ) [ne_zero n] (p : ℤ × fin n) :
⇑((int.div_mod_equiv n).symm) p = p.fst * ↑n + ↑(p.snd)
source
@[simp]
theorem fin.cast_le_order_iso_apply {n m : ℕ} (h : n ≤ m) (i : fin n) :
⇑(fin.cast_le_order_iso h) i = ⟨⇑(fin.cast_le h) i, _⟩
source
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
source
@[simp]
theorem fin.cast_le_order_iso_symm_apply {n m : ℕ} (h : n ≤ m) (i : {i // ↑i < n}) :
⇑(rel_iso.symm (fin.cast_le_order_iso h)) i = ⟨↑i, _⟩
source
@[protected, instance]
def subsingleton_fin_zero  :
subsingleton (fin 0)

fin 0 is a subsingleton.

source
@[protected, instance]
def subsingleton_fin_one  :
subsingleton (fin 1)

fin 1 is a subsingleton.