Equivalences for Fin n

def finZeroEquiv : Fin 0 ≃ Empty

Equivalence between Fin 0 and Empty.

def finZeroEquiv' : Fin 0 ≃ PEmpty.{u}

Equivalence between Fin 0 and PEmpty.

def finOneEquiv : Fin 1 ≃ Unit

Equivalence between Fin 1 and Unit.

def finTwoEquiv : Fin 2 ≃ Bool

Equivalence between Fin 2 and Bool.

@[simp]

theorem piFinTwoEquiv_apply (α : Fin 2 → Type u) : ↑(piFinTwoEquiv α) = fun f => (f 0, f 1)

@[simp]

theorem piFinTwoEquiv_symm_apply (α : Fin 2 → Type u) : ↑(piFinTwoEquiv α).symm = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

def piFinTwoEquiv (α : Fin 2 → Type u) : ((i : Fin 2) → α i) ≃ α 0 × α 1

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

theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) : (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (Fin.cons s (Fin.cons t finZeroElim))

theorem Fin.preimage_apply_01_prod' {α : Type u} (s : Set α) (t : Set α) : (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ ![s, t]

@[simp]

theorem prodEquivPiFinTwo_symm_apply (α : Type u) (β : Type u) : ↑(prodEquivPiFinTwo α β).symm = fun f => (f 0, f 1)

@[simp]

theorem prodEquivPiFinTwo_apply (α : Type u) (β : Type u) : ↑(prodEquivPiFinTwo α β) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

def prodEquivPiFinTwo (α : Type u) (β : Type u) : α × β ≃ ((i : Fin 2) → Matrix.vecCons α ![β] i)

A product space α × β is equivalent to the space Π i : Fin 2, γ i, where γ = Fin.cons α (Fin.cons β finZeroElim). See also piFinTwoEquiv and finTwoArrowEquiv.

@[simp]

theorem finTwoArrowEquiv_apply (α : Type u_1) : ↑(finTwoArrowEquiv α) = (piFinTwoEquiv fun x => α).toFun

@[simp]

theorem finTwoArrowEquiv_symm_apply (α : Type u_1) : ↑(finTwoArrowEquiv α).symm = fun x => ![x.fst, x.snd]

def finTwoArrowEquiv (α : Type u_1) : (Fin 2 → α) ≃ α × α

The space of functions Fin 2 → α is equivalent to α × α. See also piFinTwoEquiv and prodEquivPiFinTwo.

def OrderIso.piFinTwoIso (α : 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 OrderIso.finTwoArrowEquiv for a non-dependent version.

def OrderIso.finTwoArrowIso (α : Type u_1) [Preorder α] : (Fin 2 → α) ≃o α × α

The space of functions Fin 2 → α is order equivalent to α × α. See also OrderIso.piFinTwoIso.

def finCongr {m : ℕ} {n : ℕ} (h : m = n) : Fin m ≃ Fin n

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

@[simp]

theorem finCongr_apply_mk {m : ℕ} {n : ℕ} (h : m = n) (k : ℕ) (w : k < m) : ↑(finCongr h) { val := k, isLt := w } = { val := k, isLt := (_ : k < n) }

@[simp]

theorem finCongr_symm {m : ℕ} {n : ℕ} (h : m = n) : (finCongr h).symm = finCongr (_ : n = m)

@[simp]

theorem finCongr_apply_coe {m : ℕ} {n : ℕ} (h : m = n) (k : Fin m) : ↑(↑(finCongr h) k) = ↑k

theorem finCongr_symm_apply_coe {m : ℕ} {n : ℕ} (h : m = n) (k : Fin n) : ↑(↑(finCongr h).symm k) = ↑k

def finSuccEquiv' {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.predAbove that produces Option (Fin n) instead of mapping both i.cast_succ and i.succ to i.

@[simp]

theorem finSuccEquiv'_at {n : ℕ} (i : Fin (n + 1)) : ↑(finSuccEquiv' i) i = none

@[simp]

theorem finSuccEquiv'_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : ↑(finSuccEquiv' i) (Fin.succAbove i j) = some j

theorem finSuccEquiv'_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : ↑(finSuccEquiv' i) (Fin.castSucc m) = some m

theorem finSuccEquiv'_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : ↑(finSuccEquiv' i) (Fin.succ m) = some m

@[simp]

theorem finSuccEquiv'_symm_none {n : ℕ} (i : Fin (n + 1)) : ↑(finSuccEquiv' i).symm none = i

@[simp]

theorem finSuccEquiv'_symm_some {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : ↑(finSuccEquiv' i).symm (some j) = Fin.succAbove i j

theorem finSuccEquiv'_symm_some_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : ↑(finSuccEquiv' i).symm (some m) = Fin.castSucc m

theorem finSuccEquiv'_symm_some_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : ↑(finSuccEquiv' i).symm (some m) = Fin.succ m

theorem finSuccEquiv'_symm_coe_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : ↑(finSuccEquiv' i).symm (some m) = Fin.castSucc m

theorem finSuccEquiv'_symm_coe_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : ↑(finSuccEquiv' i).symm (some m) = Fin.succ m

def finSuccEquiv (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.

@[simp]

theorem finSuccEquiv_zero {n : ℕ} : ↑(finSuccEquiv n) 0 = none

@[simp]

theorem finSuccEquiv_succ {n : ℕ} (m : Fin n) : ↑(finSuccEquiv n) (Fin.succ m) = some m

@[simp]

theorem finSuccEquiv_symm_none {n : ℕ} : ↑(finSuccEquiv n).symm none = 0

@[simp]

theorem finSuccEquiv_symm_some {n : ℕ} (m : Fin n) : ↑(finSuccEquiv n).symm (some m) = Fin.succ m

theorem finSuccEquiv'_zero {n : ℕ} : finSuccEquiv' 0 = finSuccEquiv n

The equiv version of Fin.predAbove_zero.

theorem finSuccEquiv'_last_apply_castSucc {n : ℕ} (i : Fin n) : ↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some i

theorem finSuccEquiv'_last_apply {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) : ↑(finSuccEquiv' (Fin.last n)) i = some (Fin.castLT i (_ : ↑i < n))

theorem finSuccEquiv'_ne_last_apply {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) : ↑(finSuccEquiv' i) j = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) j)

def finSuccAboveEquiv {n : ℕ} (p : Fin (n + 1)) : Fin n ≃o { x // x ≠ p }

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

theorem finSuccAboveEquiv_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : ↑(finSuccAboveEquiv p) i = { val := Fin.succAbove p i, property := (_ : Fin.succAbove p i ≠ p) }

theorem finSuccAboveEquiv_symm_apply_last {n : ℕ} (x : { x // x ≠ Fin.last n }) : ↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x = Fin.castLT ↑x (_ : ↑↑x < n)

theorem finSuccAboveEquiv_symm_apply_ne_last {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x // x ≠ p }) : ↑(OrderIso.symm (finSuccAboveEquiv p)) x = Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x

def finSuccEquivLast {n : ℕ} : Fin (n + 1) ≃ Option (Fin n)

Equiv between Fin (n + 1) and Option (Fin n) sending Fin.last n to none

@[simp]

theorem finSuccEquivLast_castSucc {n : ℕ} (i : Fin n) : ↑finSuccEquivLast (Fin.castSucc i) = some i

@[simp]

theorem finSuccEquivLast_last {n : ℕ} : ↑finSuccEquivLast (Fin.last n) = none

@[simp]

theorem finSuccEquivLast_symm_some {n : ℕ} (i : Fin n) : ↑finSuccEquivLast.symm (some i) = Fin.castSucc i

@[simp]

theorem finSuccEquivLast_symm_none {n : ℕ} : ↑finSuccEquivLast.symm none = Fin.last n

@[simp]

theorem Equiv.piFinSuccAboveEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) : ↑(Equiv.piFinSuccAboveEquiv α i) = fun f => (f i, fun j => f (Fin.succAbove i j))

@[simp]

theorem Equiv.piFinSuccAboveEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) : ↑(Equiv.piFinSuccAboveEquiv α i).symm = fun f => Fin.insertNth i f.fst f.snd

def Equiv.piFinSuccAboveEquiv {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) : ((j : Fin (n + 1)) → α j) ≃ α i × ((j : Fin n) → α (Fin.succAbove i j))

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

def OrderIso.piFinSuccAboveIso {n : ℕ} (α : Fin (n + 1) → Type u) [(i : Fin (n + 1)) → LE (α i)] (i : Fin (n + 1)) : ((j : Fin (n + 1)) → α j) ≃o α i × ((j : Fin n) → α (Fin.succAbove i j))

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

@[simp]

theorem Equiv.piFinSucc_apply (n : ℕ) (β : Type u) : ↑(Equiv.piFinSucc n β) = fun f => (f 0, fun j => f (Fin.succ j))

@[simp]

theorem Equiv.piFinSucc_symm_apply (n : ℕ) (β : Type u) : ↑(Equiv.piFinSucc n β).symm = fun f => Fin.cons f.fst f.snd

def Equiv.piFinSucc (n : ℕ) (β : Type u) : (Fin (n + 1) → β) ≃ β × (Fin n → β)

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

def finSumFinEquiv {m : ℕ} {n : ℕ} : Fin m ⊕ Fin n ≃ Fin (m + n)

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

@[simp]

theorem finSumFinEquiv_apply_left {m : ℕ} {n : ℕ} (i : Fin m) : ↑finSumFinEquiv (Sum.inl i) = Fin.castAdd n i

@[simp]

theorem finSumFinEquiv_apply_right {m : ℕ} {n : ℕ} (i : Fin n) : ↑finSumFinEquiv (Sum.inr i) = Fin.natAdd m i

@[simp]

theorem finSumFinEquiv_symm_apply_castAdd {m : ℕ} {n : ℕ} (x : Fin m) : ↑finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x

@[simp]

theorem finSumFinEquiv_symm_apply_natAdd {m : ℕ} {n : ℕ} (x : Fin n) : ↑finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x

@[simp]

theorem finSumFinEquiv_symm_last {n : ℕ} : ↑finSumFinEquiv.symm (Fin.last n) = Sum.inr 0

def finAddFlip {m : ℕ} {n : ℕ} : Fin (m + n) ≃ Fin (n + m)

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

@[simp]

theorem finAddFlip_apply_castAdd {m : ℕ} (k : Fin m) (n : ℕ) : ↑finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

@[simp]

theorem finAddFlip_apply_natAdd {n : ℕ} (k : Fin n) (m : ℕ) : ↑finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

@[simp]

theorem finAddFlip_apply_mk_left {m : ℕ} {n : ℕ} {k : ℕ} (h : k < m) (hk : optParam (k < m + n) (_ : k < m + n)) (hnk : optParam (n + k < n + m) (_ : n + k < n + m)) : ↑finAddFlip { val := k, isLt := hk } = { val := n + k, isLt := hnk }

@[simp]

theorem finAddFlip_apply_mk_right {m : ℕ} {n : ℕ} {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) : ↑finAddFlip { val := k, isLt := h₂ } = { val := k - m, isLt := (_ : k - m < n + m) }

def finRotate (n : ℕ) : Equiv.Perm (Fin n)

Rotate Fin n one step to the right.

@[simp]

theorem finRotate_zero : finRotate 0 = Equiv.refl (Fin 0)

theorem finRotate_succ (n : ℕ) : finRotate (n + 1) = finAddFlip.trans (finCongr (_ : 1 + n = n + 1))

theorem finRotate_of_lt {n : ℕ} {k : ℕ} (h : k < n) : ↑(finRotate (n + 1)) { val := k, isLt := (_ : k < n + 1) } = { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ n) }

theorem finRotate_last' {n : ℕ} : ↑(finRotate (n + 1)) { val := n, isLt := (_ : n < n + 1) } = { val := 0, isLt := (_ : 0 < Nat.succ n) }

theorem finRotate_last {n : ℕ} : ↑(finRotate (n + 1)) (Fin.last n) = 0

theorem Fin.snoc_eq_cons_rotate {n : ℕ} {α : Type u_1} (v : Fin n → α) (a : α) : Fin.snoc v a = fun i => Fin.cons a v (↑(finRotate (n + 1)) i)

@[simp]

theorem finRotate_one : finRotate 1 = Equiv.refl (Fin 1)

@[simp]

theorem finRotate_succ_apply {n : ℕ} (i : Fin (n + 1)) : ↑(finRotate (n + 1)) i = i + 1

theorem finRotate_apply_zero {n : ℕ} : ↑(finRotate (Nat.succ n)) 0 = 1

theorem coe_finRotate_of_ne_last {n : ℕ} {i : Fin (Nat.succ n)} (h : i ≠ Fin.last n) : ↑(↑(finRotate (n + 1)) i) = ↑i + 1

theorem coe_finRotate {n : ℕ} (i : Fin (Nat.succ n)) : ↑(↑(finRotate (Nat.succ n)) i) = if i = Fin.last n then 0 else ↑i + 1

@[simp]

theorem finProdFinEquiv_symm_apply {m : ℕ} {n : ℕ} (x : Fin (m * n)) : ↑finProdFinEquiv.symm x = (Fin.divNat x, Fin.modNat x)

@[simp]

theorem finProdFinEquiv_apply_val {m : ℕ} {n : ℕ} (x : Fin m × Fin n) : ↑(↑finProdFinEquiv x) = ↑x.snd + n * ↑x.fst

def finProdFinEquiv {m : ℕ} {n : ℕ} : Fin m × Fin n ≃ Fin (m * n)

Equivalence between Fin m × Fin n and Fin (m * n)

@[simp]

theorem Nat.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℕ × Fin n) : ↑(Nat.divModEquiv n).symm p = p.fst * n + ↑p.snd

@[simp]

theorem Nat.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℕ) : ↑(Nat.divModEquiv n) a = (a / n, ↑a)

def Nat.divModEquiv (n : ℕ) [NeZero n] : ℕ ≃ ℕ × Fin n

The equivalence induced by a ↦ (a / n, a % n) for nonzero n. This is like finProdFinEquiv.symm but with m infinite. See Nat.div_mod_unique for a similar propositional statement.

@[simp]

theorem Int.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℤ × Fin n) : ↑(Int.divModEquiv n).symm p = p.fst * ↑n + ↑↑p.snd

@[simp]

theorem Int.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℤ) : ↑(Int.divModEquiv n) a = (a / ↑n, ↑(Int.natMod a ↑n))

def Int.divModEquiv (n : ℕ) [NeZero n] : ℤ ≃ ℤ × Fin n

The equivalence induced by a ↦ (a / n, a % n) for nonzero n. See Int.ediv_emod_unique for a similar propositional statement.

@[simp]

theorem Fin.castLEOrderIso_symm_apply {n : ℕ} {m : ℕ} (h : n ≤ m) (i : { i // ↑i < n }) : ↑(RelIso.symm (Fin.castLEOrderIso h)) i = { val := ↑↑i, isLt := (_ : ↑↑i < n) }

@[simp]

theorem Fin.castLEOrderIso_apply {n : ℕ} {m : ℕ} (h : n ≤ m) (i : Fin n) : ↑(Fin.castLEOrderIso h) i = { val := Fin.castLE h i, property := (_ : ↑i < n) }

def Fin.castLEOrderIso {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 OrderIso version of Fin.castLE.

instance subsingleton_fin_zero : Subsingleton (Fin 0)

Fin 0 is a subsingleton.

instance subsingleton_fin_one : Subsingleton (Fin 1)

Fin 1 is a subsingleton.