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.

Equivalence between fin 0 and empty.

Equations

Equivalence between fin 0 and pempty.

Equations

Equivalence between fin 1 and unit.

Equations

Equivalence between fin 2 and bool.

Equations
@[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)
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
@[simp]
theorem pi_fin_two_equiv_apply (α : fin 2 Type u) :
(pi_fin_two_equiv α) = λ (f : Π (i : fin 2), α i), (f 0, f 1)
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))
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]
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
@[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)
@[simp]
theorem fin_two_arrow_equiv_apply (α : Type u_1) :
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
@[simp]
theorem fin_two_arrow_equiv_symm_apply (α : Type u_1) :
((fin_two_arrow_equiv α).symm) = λ (x : α × α), ![x.fst, x.snd]
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
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
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 + 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
@[simp]
theorem fin_succ_equiv'_at {n : } (i : fin (n + 1)) :
@[simp]
theorem fin_succ_equiv'_succ_above {n : } (i : fin (n + 1)) (j : fin n) :
theorem fin_succ_equiv'_below {n : } {i : fin (n + 1)} {m : fin n} (h : fin.cast_succ m < i) :
theorem fin_succ_equiv'_above {n : } {i : fin (n + 1)} {m : fin n} (h : i fin.cast_succ m) :
@[simp]
theorem fin_succ_equiv'_symm_none {n : } (i : fin (n + 1)) :
@[simp]
theorem fin_succ_equiv'_symm_some {n : } (i : fin (n + 1)) (j : fin n) :
theorem fin_succ_equiv'_symm_some_above {n : } {i : fin (n + 1)} {m : fin n} (h : i fin.cast_succ m) :
theorem fin_succ_equiv'_symm_coe_below {n : } {i : fin (n + 1)} {m : fin n} (h : fin.cast_succ m < i) :
theorem fin_succ_equiv'_symm_coe_above {n : } {i : fin (n + 1)} {m : fin n} (h : i fin.cast_succ 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]
@[simp]
theorem fin_succ_equiv_succ {n : } (m : fin n) :
@[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'_last_apply {n : } {i : fin (n + 1)} (h : i fin.last n) :
theorem fin_succ_equiv'_ne_last_apply {n : } {i j : fin (n + 1)} (hi : i fin.last n) (hj : j i) :
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
theorem fin_succ_above_equiv_apply {n : } (p : fin (n + 1)) (i : fin n) :
theorem fin_succ_above_equiv_symm_apply_ne_last {n : } {p : fin (n + 1)} (h : p fin.last n) (x : {x // x p}) :
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
@[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
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
@[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))
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
def equiv.pi_fin_succ (n : ) (β : Type u) :
(fin (n + 1) β) β × (fin n β)

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

Equations
@[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
@[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)
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
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_cast_add {m : } (k : fin m) (n : ) :
@[simp]
theorem fin_add_flip_apply_nat_add {n : } (k : fin n) (m : ) :
@[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⟩
@[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, _⟩
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 : α) :
fin.snoc v a = λ (i : fin (n + 1)), fin.cons a v ((fin_rotate (n + 1)) i)
@[simp]
@[simp]
@[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 fin.last n) :
theorem coe_fin_rotate {n : } (i : fin n.succ) :
((fin_rotate n.succ) i) = ite (i = fin.last n) 0 (i + 1)
@[simp]
theorem fin_prod_fin_equiv_symm_apply {m n : } (x : fin (m * n)) :
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_prod_fin_equiv_apply_val {m n : } (x : fin m × fin n) :
@[simp]
theorem nat.div_mod_equiv_apply (n : ) [ne_zero n] (a : ) :
(n.div_mod_equiv) a = (a / n, a)
def nat.div_mod_equiv (n : ) [ne_zero 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
@[simp]
theorem nat.div_mod_equiv_symm_apply (n : ) [ne_zero n] (p : × fin n) :
@[simp]
theorem int.div_mod_equiv_apply (n : ) [ne_zero n] (a : ) :
def int.div_mod_equiv (n : ) [ne_zero n] :

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

See int.div_mod_unique for a similar propositional statement.

Equations
@[simp]
theorem int.div_mod_equiv_symm_apply (n : ) [ne_zero n] (p : × fin n) :
@[simp]
theorem fin.cast_le_order_iso_apply {n m : } (h : n m) (i : fin n) :
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}) :
@[protected, instance]

fin 0 is a subsingleton.

@[protected, instance]

fin 1 is a subsingleton.