Embeddings of Fin n

Fin n is the type whose elements are natural numbers smaller than n. This file defines embeddings between Fin n and other types,

Main definitions

• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.succEmb : Fin.succ as an Embedding;
• Fin.castLEEmb h : Fin.castLE as an Embedding, embed Fin n into Fin m, h : n ≤ m;
• finCongr : Fin.cast as an Equiv, equivalence between Fin n and Fin m when n = m;
• Fin.castAddEmb m : Fin.castAdd as an Embedding, embed Fin n into Fin (n+m);
• Fin.castSuccEmb : Fin.castSucc as an Embedding, embed Fin n into Fin (n+1);
• Fin.addNatEmb m i : Fin.addNat as an Embedding, add m on i on the right, generalizes Fin.succ;
• Fin.natAddEmb n i : Fin.natAdd as an Embedding, adds n on i on the left;

order

def Fin.valEmbedding {n : ℕ} : Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

• Fin.valEmbedding = { toFun := Fin.val, inj' := ⋯ }

@[simp]

theorem Fin.valEmbedding_apply {n : ℕ} : ⇑valEmbedding = val

@[simp]

theorem Fin.equivSubtype_symm_trans_valEmbedding {n : ℕ} : equivSubtype.symm.toEmbedding.trans valEmbedding = Function.Embedding.subtype fun (x : ℕ) => x < n

succ and casts into larger Fin types

def Fin.succEmb (n : ℕ) : Fin n ↪ Fin (n + 1)

Fin.succ as an Embedding

Equations

• Fin.succEmb n = { toFun := Fin.succ, inj' := ⋯ }

@[simp]

theorem Fin.coe_succEmb {n : ℕ} : ⇑(succEmb n) = succ

@[deprecated Fin.coe_succEmb (since := "2025-04-12")]

theorem Fin.val_succEmb {n : ℕ} : ⇑(succEmb n) = succ

Alias of Fin.coe_succEmb.

def Fin.castLEEmb {n m : ℕ} (h : n ≤ m) : Fin n ↪ Fin m

Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

Equations

• Fin.castLEEmb h = { toFun := Fin.castLE h, inj' := ⋯ }

@[simp]

theorem Fin.castLEEmb_apply {n m : ℕ} (h : n ≤ m) (i : Fin n) : (castLEEmb h) i = castLE h i

@[simp]

theorem Fin.coe_castLEEmb {m n : ℕ} (hmn : m ≤ n) : ⇑(castLEEmb hmn) = castLE hmn

theorem Fin.nonempty_embedding_iff {n m : ℕ} : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

theorem Fin.equiv_iff_eq {n m : ℕ} : Nonempty (Fin m ≃ Fin n) ↔ m = n

def Fin.castAddEmb {n : ℕ} (m : ℕ) : Fin n ↪ Fin (n + m)

Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

Equations

• Fin.castAddEmb m = Fin.castLEEmb ⋯

@[simp]

theorem Fin.coe_castAddEmb {n : ℕ} (m : ℕ) : ⇑(castAddEmb m) = castAdd m

theorem Fin.castAddEmb_apply {n : ℕ} (m : ℕ) (i : Fin n) : (castAddEmb m) i = castAdd m i

def Fin.castSuccEmb {n : ℕ} : Fin n ↪ Fin (n + 1)

Fin.castSucc as an Embedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

Equations

• Fin.castSuccEmb = Fin.castAddEmb 1

@[simp]

theorem Fin.coe_castSuccEmb {n : ℕ} : ⇑castSuccEmb = castSucc

theorem Fin.castSuccEmb_apply {n : ℕ} (i : Fin n) : castSuccEmb i = i.castSucc

def Fin.addNatEmb {n : ℕ} (m : ℕ) : Fin n ↪ Fin (n + m)

Fin.addNat as an Embedding, addNatEmb m i adds m to i, generalizes Fin.succ.

Equations

• Fin.addNatEmb m = { toFun := fun (x : Fin n) => x.addNat m, inj' := ⋯ }

@[simp]

theorem Fin.addNatEmb_apply {n : ℕ} (m : ℕ) (x✝ : Fin n) : (addNatEmb m) x✝ = x✝.addNat m

def Fin.natAddEmb (n : ℕ) {m : ℕ} : Fin m ↪ Fin (n + m)

Fin.natAdd as an Embedding, natAddEmb n i adds n to i "on the left".

Equations

• Fin.natAddEmb n = { toFun := Fin.natAdd n, inj' := ⋯ }

@[simp]

theorem Fin.natAddEmb_apply (n : ℕ) {m : ℕ} (i : Fin m) : (natAddEmb n) i = natAdd n i

def Fin.succAboveEmb {n : ℕ} (p : Fin (n + 1)) : Fin n ↪ Fin (n + 1)

Fin.succAbove p as an Embedding.

Equations

• p.succAboveEmb = { toFun := p.succAbove, inj' := ⋯ }

@[simp]

theorem Fin.succAboveEmb_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveEmb i = p.succAbove i

@[simp]

theorem Fin.coe_succAboveEmb {n : ℕ} (p : Fin (n + 1)) : ⇑p.succAboveEmb = p.succAbove