Equivalences for `Fin n` #

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the first element of the tuple.

This is Fin.cons as an Equiv.

Equations

Fin.consEquiv α = { toFun := fun (f : α 0 × ((i : Fin n) → α i.succ)) => Fin.cons f.1 f.2, invFun := fun (f : (i : Fin (n + 1)) → α i) => (f 0, Fin.tail f), left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem Fin.snocEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : α (Fin.last n) × ((i : Fin n) → α i.castSucc)) :

∀ (x : Fin (n + 1)), (Fin.snocEquiv α) f x = Fin.snoc f.2 f.1 x

source

@[simp]

theorem Fin.snocEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : (i : Fin (n + 1)) → α i) :

(Fin.snocEquiv α).symm f = (f (Fin.last n), Fin.init f)

source

def Fin.snocEquiv {n : ℕ} (α : Fin (n + 1) → Type u_1) :

α (Fin.last n) × ((i : Fin n) → α i.castSucc) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the last element of the tuple.

This is Fin.snoc as an Equiv.

Equations

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

source

@[simp]

theorem Fin.insertNthEquiv_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) :

(Fin.insertNthEquiv α p).symm f = (f p, p.removeNth f)

source

@[simp]

theorem Fin.insertNthEquiv_apply {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)) :

(Fin.insertNthEquiv α p) f j = p.insertNth f.1 f.2 j

source

def Fin.insertNthEquiv {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) :

α p × ((i : Fin n) → α (p.succAbove i)) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple.

This is Fin.insertNth as an Equiv.

Equations

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

source

@[simp]

theorem Fin.insertNthEquiv_zero {n : ℕ} (α : Fin (n + 1) → Type u_1) :

Fin.insertNthEquiv α 0 = Fin.consEquiv α

source

@[simp]

theorem Fin.insertNthEquiv_last (n : ℕ) (α : Type u_1) :

Fin.insertNthEquiv (fun (x : Fin (n + 1)) => α) (Fin.last n) = Fin.snocEquiv fun (x : Fin (n + 1)) => α

Note this lemma can only be written about non-dependent tuples as insertNth (last n) = snoc is not a definitional equality.

source

@[simp]

theorem piFinTwoEquiv_apply (α : Fin 2 → Type u) :

⇑(piFinTwoEquiv α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)

source

@[simp]

theorem piFinTwoEquiv_symm_apply (α : Fin 2 → Type u) :

⇑(piFinTwoEquiv α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

source

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.

Equations

piFinTwoEquiv α = { toFun := fun (f : (i : Fin 2) → α i) => (f 0, f 1), invFun := fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim), left_inv := ⋯, right_inv := ⋯ }

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 (Fin.cons s (Fin.cons t finZeroElim))

source

theorem Fin.preimage_apply_01_prod' {α : Type u} (s : Set α) (t : Set α) :

(fun (f : Fin 2 → α) => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi ![s, t]

source

@[simp]

theorem prodEquivPiFinTwo_apply (α : Type u) (β : 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

@[simp]

theorem prodEquivPiFinTwo_symm_apply (α : Type u) (β : Type u) :

⇑(prodEquivPiFinTwo α β).symm = fun (f : (i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) => (f 0, f 1)

source

def prodEquivPiFinTwo (α : Type u) (β : 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

source

@[simp]

theorem finTwoArrowEquiv_apply (α : Type u_1) :

⇑(finTwoArrowEquiv α) = (piFinTwoEquiv fun (x : Fin 2) => α).toFun

source

@[simp]

theorem finTwoArrowEquiv_symm_apply (α : Type u_1) :

⇑(finTwoArrowEquiv α).symm = fun (x : α × α) => ![x.1, x.2]

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 := ⋯ }

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.cast_succ 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 := ⋯ }

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

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

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

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 : Fin (n + 1)} {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, ⋯⟩

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)

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

@[simp]

theorem Equiv.piFinSuccAbove_apply {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) :

⇑(Equiv.piFinSuccAbove α i) = fun (f : (j : Fin (n + 1)) → α j) => (f i, i.removeNth f)

source

@[simp]

theorem Equiv.piFinSuccAbove_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) :

⇑(Equiv.piFinSuccAbove α i).symm = fun (f : α i × ((j : Fin n) → α (i.succAbove j))) => i.insertNth f.1 f.2

source

@[deprecated Fin.insertNthEquiv]

def Equiv.piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type u) (i : Fin (n + 1)) :

((j : Fin (n + 1)) → α j) ≃ α i × ((j : Fin n) → α (i.succAbove j))

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

Equations

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

source

@[simp]

theorem Equiv.piFinSucc_symm_apply (n : ℕ) (β : Type u) :

⇑(Equiv.piFinSucc n β).symm = ⇑(Fin.consEquiv fun (x : Fin (n + 1)) => β)

source

@[simp]

theorem Equiv.piFinSucc_apply (n : ℕ) (β : Type u) :

⇑(Equiv.piFinSucc n β) = ⇑(Fin.consEquiv fun (x : Fin (n + 1)) => β).symm

source

@[deprecated Fin.consEquiv]

def Equiv.piFinSucc (n : ℕ) (β : Type u) :

(Fin (n + 1) → β) ≃ β × (Fin n → β)

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

Equations

Equiv.piFinSucc n β = (Fin.insertNthEquiv (fun (x : Fin (n + 1)) => β) 0).symm

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) ι)

source

@[simp]

theorem Equiv.embeddingFinSucc_fst {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) :

⇑((Equiv.embeddingFinSucc n ι) e).fst = ⇑e ∘ Fin.succ

source

@[simp]

theorem Equiv.embeddingFinSucc_snd {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) :

↑((Equiv.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 }) :

⇑((Equiv.embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst

source

@[simp]

theorem Equiv.piFinCastSucc_apply (n : ℕ) (β : Type u) :

⇑(Equiv.piFinCastSucc n β) = ⇑(Fin.snocEquiv fun (x : Fin (n + 1)) => β).symm

source

@[simp]

theorem Equiv.piFinCastSucc_symm_apply (n : ℕ) (β : Type u) :

⇑(Equiv.piFinCastSucc n β).symm = ⇑(Fin.snocEquiv fun (x : Fin (n + 1)) => β)

source

@[deprecated Fin.snocEquiv]

def Equiv.piFinCastSucc (n : ℕ) (β : Type u) :

(Fin (n + 1) → β) ≃ β × (Fin n → β)

Equivalence between Fin (n + 1) → β and β × (Fin n → β) which separates out the last element of the tuple.

Equations

Equiv.piFinCastSucc n β = (Fin.insertNthEquiv (fun (x : Fin (n + 1)) => β) (Fin.last n)).symm

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 := ⋯ }

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_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 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

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 : optParam (k < m + n) ⋯) (hnk : optParam (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 finRotate (n : ℕ) :

Equiv.Perm (Fin n)

Rotate Fin n one step to the right.

Equations

finRotate 0 = Equiv.refl (Fin 0)
finRotate n.succ = finAddFlip.trans (finCongr ⋯)

source

@[simp]

theorem finRotate_zero :

finRotate 0 = Equiv.refl (Fin 0)

source

theorem finRotate_succ (n : ℕ) :

finRotate (n + 1) = finAddFlip.trans (finCongr ⋯)

source

theorem finRotate_of_lt {n : ℕ} {k : ℕ} (h : k < n) :

(finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

source

theorem finRotate_last' {n : ℕ} :

(finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩

source

theorem finRotate_last {n : ℕ} :

(finRotate (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 = fun (i : Fin (n + 1)) => Fin.cons a v ((finRotate (n + 1)) i)

source

@[simp]

theorem finRotate_one :

finRotate 1 = Equiv.refl (Fin 1)

source

@[simp]

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

(finRotate (n + 1)) i = i + 1

source

theorem finRotate_apply_zero {n : ℕ} :

(finRotate n.succ) 0 = 1

source

theorem coe_finRotate_of_ne_last {n : ℕ} {i : Fin n.succ} (h : i ≠ Fin.last n) :

↑((finRotate (n + 1)) i) = ↑i + 1

source

theorem coe_finRotate {n : ℕ} (i : Fin n.succ) :

↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1

source

@[simp]

theorem finProdFinEquiv_symm_apply {m : ℕ} {n : ℕ} (x : Fin (m * n)) :

finProdFinEquiv.symm x = (x.divNat, x.modNat)

source

@[simp]

theorem finProdFinEquiv_apply_val {m : ℕ} {n : ℕ} (x : Fin m × Fin n) :

↑(finProdFinEquiv x) = ↑x.2 + n * ↑x.1

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 := ⋯ }

source

@[simp]

theorem Nat.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℕ × Fin n) :

n.divModEquiv.symm p = p.1 * n + ↑p.2

source

@[simp]

theorem Nat.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℕ) :

n.divModEquiv a = (a / n, ↑a)

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, ↑a), invFun := fun (p : ℕ × Fin n) => p.1 * n + ↑p.2, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem Int.divModEquiv_symm_apply (n : ℕ) [NeZero n] (p : ℤ × Fin n) :

(Int.divModEquiv n).symm p = p.1 * ↑n + ↑↑p.2

source

@[simp]

theorem Int.divModEquiv_apply (n : ℕ) [NeZero n] (a : ℤ) :

(Int.divModEquiv n) a = (a / ↑n, ↑(a.natMod ↑n))

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, ↑(a.natMod ↑n)), invFun := fun (p : ℤ × Fin n) => p.1 * ↑n + ↑↑p.2, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem Fin.castLEquiv_apply {n : ℕ} {m : ℕ} (h : n ≤ m) (i : Fin n) :

(Fin.castLEquiv h) i = ⟨Fin.castLE h i, ⋯⟩

source

@[simp]

theorem Fin.castLEquiv_symm_apply {n : ℕ} {m : ℕ} (h : n ≤ m) (i : { i : Fin m // ↑i < n }) :

(Fin.castLEquiv h).symm i = ⟨↑↑i, ⋯⟩

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 := ⋯ }