# Equivalences for `Fin n` #

### Miscellaneous #

This is currently not very sorted. PRs welcome!

source
theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) :
(fun (f : (i : Fin 2) → α i) => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (cons s (cons t finZeroElim))
source
theorem Fin.preimage_apply_01_prod' {α : Type u} (s t : Set α) :
(fun (f : Fin 2 → α) => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi ![s, t]
source
def prodEquivPiFinTwo (α β : Type u) :
α × β ≃ ((i : Fin 2) → ![α, β] i)

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

Equations

- prodEquivPiFinTwo α β = (piFinTwoEquiv (Fin.cons α (Fin.cons β finZeroElim))).symm

Instances For

source
@[simp]
theorem prodEquivPiFinTwo_symm_apply (α β : Type u) :
⇑(prodEquivPiFinTwo α β).symm = fun (f : (i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) => (f 0, f 1)
source
@[simp]
theorem prodEquivPiFinTwo_apply (α β : Type u) :
⇑(prodEquivPiFinTwo α β) = fun (p : Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
source
def finTwoArrowEquiv (α : Type u_1) :
(Fin 2 → α) ≃ α × α

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

Equations

- finTwoArrowEquiv α = { toFun := (piFinTwoEquiv fun (x : Fin 2) => α).toFun, invFun := fun (x : α × α) => ![x.1, x.2], left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finTwoArrowEquiv_symm_apply (α : Type u_1) :
⇑(finTwoArrowEquiv α).symm = fun (x : α × α) => ![x.1, x.2]
source
@[simp]
theorem finTwoArrowEquiv_apply (α : Type u_1) :
⇑(finTwoArrowEquiv α) = (piFinTwoEquiv fun (x : Fin 2) => α).toFun
source
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.castSucc` and `i.succ` to `i`.

Equations

- finSuccEquiv' i = { toFun := i.insertNth none some, invFun := fun (x : Option (Fin n)) => x.casesOn' i i.succAbove, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finSuccEquiv'_at {n : ℕ} (i : Fin (n + 1)) :
(finSuccEquiv' i) i = none
source
@[simp]
theorem finSuccEquiv'_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(finSuccEquiv' i) (i.succAbove j) = some j
source
theorem finSuccEquiv'_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
(finSuccEquiv' i) m.castSucc = some m
source
theorem finSuccEquiv'_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ m.castSucc) :
(finSuccEquiv' i) m.succ = some m
source
@[simp]
theorem finSuccEquiv'_symm_none {n : ℕ} (i : Fin (n + 1)) :
(finSuccEquiv' i).symm none = i
source
@[simp]
theorem finSuccEquiv'_symm_some {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(finSuccEquiv' i).symm (some j) = i.succAbove j
source
@[simp]
theorem finSuccEquiv'_eq_some {n : ℕ} {i j : Fin (n + 1)} {k : Fin n} :
(finSuccEquiv' i) j = some k ↔ j = i.succAbove k
source
@[simp]
theorem finSuccEquiv'_eq_none {n : ℕ} {i j : Fin (n + 1)} :
(finSuccEquiv' i) j = none ↔ i = j
source
theorem finSuccEquiv'_symm_some_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
(finSuccEquiv' i).symm (some m) = m.castSucc
source
theorem finSuccEquiv'_symm_some_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ m.castSucc) :
(finSuccEquiv' i).symm (some m) = m.succ
source
theorem finSuccEquiv'_symm_coe_below {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
(finSuccEquiv' i).symm (some m) = m.castSucc
source
theorem finSuccEquiv'_symm_coe_above {n : ℕ} {i : Fin (n + 1)} {m : Fin n} (h : i ≤ m.castSucc) :
(finSuccEquiv' i).symm (some m) = m.succ
source
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`.

Equations

- finSuccEquiv n = finSuccEquiv' 0

Instances For

source
@[simp]
theorem finSuccEquiv_zero {n : ℕ} :
(finSuccEquiv n) 0 = none
source
@[simp]
theorem finSuccEquiv_succ {n : ℕ} (m : Fin n) :
(finSuccEquiv n) m.succ = some m
source
@[simp]
theorem finSuccEquiv_symm_none {n : ℕ} :
(finSuccEquiv n).symm none = 0
source
@[simp]
theorem finSuccEquiv_symm_some {n : ℕ} (m : Fin n) :
(finSuccEquiv n).symm (some m) = m.succ
source
@[simp]
theorem finSuccEquiv_eq_some {n : ℕ} {i : Fin (n + 1)} {j : Fin n} :
(finSuccEquiv n) i = some j ↔ i = j.succ
source
@[simp]
theorem finSuccEquiv_eq_none {n : ℕ} {i : Fin (n + 1)} :
(finSuccEquiv n) i = none ↔ i = 0
source
theorem finSuccEquiv'_zero {n : ℕ} :
finSuccEquiv' 0 = finSuccEquiv n

The equiv version of `Fin.predAbove_zero`.

source
theorem finSuccEquiv'_last_apply_castSucc {n : ℕ} (i : Fin n) :
(finSuccEquiv' (Fin.last n)) i.castSucc = some i
source
theorem finSuccEquiv'_last_apply {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) :
(finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)
source
theorem finSuccEquiv'_ne_last_apply {n : ℕ} {i j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) :
(finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)
source
def finSuccAboveEquiv {n : ℕ} (p : Fin (n + 1)) :
Fin n ≃ { x : Fin (n + 1) // x ≠ p }

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

Equations

- finSuccAboveEquiv p = (Equiv.optionSubtype p) ⟨(finSuccEquiv' p).symm, ⋯⟩

Instances For

source
theorem finSuccAboveEquiv_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
(finSuccAboveEquiv p) i = ⟨p.succAbove i, ⋯⟩
source
theorem finSuccAboveEquiv_symm_apply_last {n : ℕ} (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
(finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯
source
theorem finSuccAboveEquiv_symm_apply_ne_last {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x : Fin (n + 1) // x ≠ p }) :
(finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
source
def finSuccEquivLast {n : ℕ} :
Fin (n + 1) ≃ Option (Fin n)

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

Equations

- finSuccEquivLast = finSuccEquiv' (Fin.last n)

Instances For

source
@[simp]
theorem finSuccEquivLast_castSucc {n : ℕ} (i : Fin n) :
finSuccEquivLast i.castSucc = some i
source
@[simp]
theorem finSuccEquivLast_last {n : ℕ} :
finSuccEquivLast (Fin.last n) = none
source
@[simp]
theorem finSuccEquivLast_symm_some {n : ℕ} (i : Fin n) :
finSuccEquivLast.symm (some i) = i.castSucc
source
@[simp]
theorem finSuccEquivLast_symm_none {n : ℕ} :
finSuccEquivLast.symm none = Fin.last n
source
def Equiv.embeddingFinSucc (n : ℕ) (ι : Type u_1) :
(Fin (n + 1) ↪ ι) ≃ (e : Fin n ↪ ι) × { i : ι // i ∉ Set.range ⇑e }

An embedding `e : Fin (n+1) ↪ ι` corresponds to an embedding `f : Fin n ↪ ι` (corresponding the last `n` coordinates of `e`) together with a value not taken by `f` (corresponding to `e 0`).

Equations

- Equiv.embeddingFinSucc n ι = ((finSuccEquiv n).embeddingCongr (Equiv.refl ι)).trans (Function.Embedding.optionEmbeddingEquiv (Fin n) ι)

Instances For

source
@[simp]
theorem Equiv.embeddingFinSucc_fst {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) :
⇑((embeddingFinSucc n ι) e).fst = ⇑e ∘ Fin.succ
source
@[simp]
theorem Equiv.embeddingFinSucc_snd {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) :
↑((embeddingFinSucc n ι) e).snd = e 0
source
@[simp]
theorem Equiv.coe_embeddingFinSucc_symm {n : ℕ} {ι : Type u_1} (f : (e : Fin n ↪ ι) × { i : ι // i ∉ Set.range ⇑e }) :
⇑((embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst
source
def finSumFinEquiv {m n : ℕ} :
Fin m ⊕ Fin n ≃ Fin (m + n)

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

Equations

- finSumFinEquiv = { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m), invFun := fun (i : Fin (m + n)) => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finSumFinEquiv_apply_left {m n : ℕ} (i : Fin m) :
finSumFinEquiv (Sum.inl i) = Fin.castAdd n i
source
@[simp]
theorem finSumFinEquiv_apply_right {m n : ℕ} (i : Fin n) :
finSumFinEquiv (Sum.inr i) = Fin.natAdd m i
source
@[simp]
theorem finSumFinEquiv_symm_apply_castAdd {m n : ℕ} (x : Fin m) :
finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x
source
@[simp]
theorem finSumFinEquiv_symm_apply_castSucc {m : ℕ} (x : Fin m) :
finSumFinEquiv.symm x.castSucc = Sum.inl x
source
@[simp]
theorem finSumFinEquiv_symm_apply_natAdd {m n : ℕ} (x : Fin n) :
finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x
source
@[simp]
theorem finSumFinEquiv_symm_last {n : ℕ} :
finSumFinEquiv.symm (Fin.last n) = Sum.inr 0
source
def finSumNatEquiv (n : ℕ) :
Fin n ⊕ ℕ ≃ ℕ

Equivalence between `Fin n ⊕ ℕ` and `ℕ` that sends `inl (a : Fin n)` to `(a : ℕ)` and `inr a` to `n + a`.

Equations

- finSumNatEquiv n = { toFun := Sum.elim Fin.val fun (x : ℕ) => n + x, invFun := fun (i : ℕ) => if hi : i < n then Sum.inl ⟨i, hi⟩ else Sum.inr (i - n), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finSumNatEquiv_apply_left {n : ℕ} (i : Fin n) :
(finSumNatEquiv n) (Sum.inl i) = ↑i
source
@[simp]
theorem finSumNatEquiv_apply_right {n : ℕ} (i : ℕ) :
(finSumNatEquiv n) (Sum.inr i) = n + i
source
@[simp]
theorem finSumNatEquiv_symm_apply_of_lt {n i : ℕ} (hi : i < n) :
(finSumNatEquiv n).symm i = Sum.inl ⟨i, hi⟩
source
@[simp]
theorem finSumNatEquiv_symm_apply_of_ge {n i : ℕ} (hi : n ≤ i) :
(finSumNatEquiv n).symm i = Sum.inr (i - n)
source
theorem finSumNatEquiv_symm_apply_fin {n : ℕ} (i : Fin n) :
(finSumNatEquiv n).symm ↑i = Sum.inl i
source
theorem finSumNatEquiv_symm_apply_add_left {n : ℕ} (i : ℕ) :
(finSumNatEquiv n).symm (i + n) = Sum.inr i
source
theorem finSumNatEquiv_symm_apply_add_right {n : ℕ} (i : ℕ) :
(finSumNatEquiv n).symm (n + i) = Sum.inr i
source
@[simp]
theorem isLeft_finSumNatEquiv_symm_apply {n : ℕ} (i : ℕ) :
((finSumNatEquiv n).symm i).isLeft = decide (i < n)
source
@[simp]
theorem isRight_finSumNatEquiv_symm_apply {n : ℕ} (i : ℕ) :
((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)
source
def finAddFlip {m n : ℕ} :
Fin (m + n) ≃ Fin (n + m)

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

Equations

- finAddFlip = (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin m) (Fin n))).trans finSumFinEquiv

Instances For

source
@[simp]
theorem finAddFlip_apply_castAdd {m : ℕ} (k : Fin m) (n : ℕ) :
finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
source
@[simp]
theorem finAddFlip_apply_natAdd {n : ℕ} (k : Fin n) (m : ℕ) :
finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
source
@[simp]
theorem finAddFlip_apply_mk_left {m n k : ℕ} (h : k < m) (hk : k < m + n := ⋯) (hnk : n + k < n + m := ⋯) :
finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩
source
@[simp]
theorem finAddFlip_apply_mk_right {m n k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩
source
def finProdFinEquiv {m n : ℕ} :
Fin m × Fin n ≃ Fin (m * n)

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

Equations

- finProdFinEquiv = { toFun := fun (x : Fin m × Fin n) => ⟨↑x.2 + n * ↑x.1, ⋯⟩, invFun := fun (x : Fin (m * n)) => (x.divNat, x.modNat), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finProdFinEquiv_apply_val {m n : ℕ} (x : Fin m × Fin n) :
↑(finProdFinEquiv x) = ↑x.2 + n * ↑x.1
source
@[simp]
theorem finProdFinEquiv_symm_apply {m n : ℕ} (x : Fin (m * n)) :
finProdFinEquiv.symm x = (x.divNat, x.modNat)
source
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.

Equations

- n.divModEquiv = { toFun := fun (a : ℕ) => (a / n, Fin.ofNat n a), invFun := fun (p : ℕ × Fin n) => p.1 * n + ↑p.2, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Nat.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℕ) :
n.divModEquiv a = (a / n, Fin.ofNat n a)
source
@[simp]
theorem Nat.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℕ × Fin n) :
n.divModEquiv.symm p = p.1 * n + ↑p.2
source
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.

Equations

- Int.divModEquiv n = { toFun := fun (a : ℤ) => (a / ↑n, Fin.ofNat n (a.natMod ↑n)), invFun := fun (p : ℤ × Fin n) => p.1 * ↑n + ↑↑p.2, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Int.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℤ × Fin n) :
(divModEquiv n).symm p = p.1 * ↑n + ↑↑p.2
source
@[simp]
theorem Int.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℤ) :
(divModEquiv n) a = (a / ↑n, Fin.ofNat n (a.natMod ↑n))
source
def Fin.castLEquiv {n m : ℕ} (h : n ≤ m) :
Fin n ≃ { i : Fin m // ↑i < n }

Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying values are retained.

This is the `Equiv` version of `Fin.castLE`.

Equations

- Fin.castLEquiv h = { toFun := fun (i : Fin n) => ⟨Fin.castLE h i, ⋯⟩, invFun := fun (i : { i : Fin m // ↑i < n }) => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Fin.castLEquiv_symm_apply {n m : ℕ} (h : n ≤ m) (i : { i : Fin m // ↑i < n }) :
(castLEquiv h).symm i = ⟨↑↑i, ⋯⟩
source
@[simp]
theorem Fin.castLEquiv_apply {n m : ℕ} (h : n ≤ m) (i : Fin n) :
(castLEquiv h) i = ⟨castLE h i, ⋯⟩
source
@[deprecated Fin.subsingleton_zero (since := "2025-06-03")]
theorem subsingleton_fin_zero :
Subsingleton (Fin 0)
source
@[deprecated Fin.subsingleton_one (since := "2025-06-03")]
theorem subsingleton_fin_one :
Subsingleton (Fin 1)
source
def Fin.appendEquiv {α : Type u_1} (m n : ℕ) :
(Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α)

The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Fin.appendEquiv_apply {α : Type u_1} (m n : ℕ) (fg : (Fin m → α) × (Fin n → α)) (a✝ : Fin (m + n)) :
(appendEquiv m n) fg a✝ = append fg.1 fg.2 a✝
source
@[simp]
theorem Fin.appendEquiv_symm_apply {α : Type u_1} (m n : ℕ) (f : Fin (m + n) → α) :
(appendEquiv m n).symm f = (fun (i : Fin m) => f (castAdd n i), fun (i : Fin n) => f (natAdd m i))
source
def Fin.succFunEquiv (α : Type u_1) (n : ℕ) :
(Fin (n + 1) → α) ≃ (Fin n → α) × α

`Fin (n + 1) → α` and `(Fin n → α) × α` are equivalent.

Equations

- Fin.succFunEquiv α n = (Fin.appendEquiv n 1).symm.trans (Equiv.prodCongrRight fun (x : Fin n → α) => Equiv.funUnique (Fin 1) α)

Instances For

source
@[simp]
theorem Fin.succFunEquiv_apply (α : Type u_1) (n : ℕ) (a✝ : Fin (n + 1) → α) :
(succFunEquiv α n) a✝ = (fun (i : Fin n) => a✝ (castAdd 1 i), a✝ (natAdd n 0))
source
@[simp]
theorem Fin.succFunEquiv_symm_apply (α : Type u_1) (n : ℕ) (a✝ : (Fin n → α) × α) (a✝¹ : Fin (n + 1)) :
(succFunEquiv α n).symm a✝ a✝¹ = append ((Equiv.prodCongrRight fun (x : Fin n → α) => Equiv.funUnique (Fin 1) α).symm a✝).1 ((Equiv.prodCongrRight fun (x : Fin n → α) => Equiv.funUnique (Fin 1) α).symm a✝).2 a✝¹