Equivalences for Fin n#

Equivalence between Fin 0 and Empty.

Equations
Instances For

Equivalence between Fin 0 and PEmpty.

Equations
Instances For

Equivalence between Fin 1 and Unit.

Equations
Instances For

Equivalence between Fin 2 and Bool.

Equations
Instances For
@[simp]
theorem piFinTwoEquiv_apply (α : Fin 2Type u) :
() = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
@[simp]
theorem piFinTwoEquiv_symm_apply (α : Fin 2Type u) :
().symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
def piFinTwoEquiv (α : Fin 2Type 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
• = { 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 := }
Instances For
theorem Fin.preimage_apply_01_prod {α : Fin 2Type 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))
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]
@[simp]
theorem prodEquivPiFinTwo_symm_apply (α : Type u) (β : Type u) :
().symm = fun (f : (i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) => (f 0, f 1)
@[simp]
theorem prodEquivPiFinTwo_apply (α : Type u) (β : Type u) :
() = fun (p : Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
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
Instances For
@[simp]
theorem finTwoArrowEquiv_symm_apply (α : Type u_1) :
().symm = fun (x : α × α) => ![x.1, x.2]
@[simp]
theorem finTwoArrowEquiv_apply (α : Type u_1) :
() = (piFinTwoEquiv fun (x : Fin 2) => α).toFun
def finTwoArrowEquiv (α : Type u_1) :
(Fin 2α) α × α

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

Equations
• = let __src := piFinTwoEquiv fun (x : Fin 2) => α; { toFun := __src.toFun, invFun := fun (x : α × α) => ![x.1, x.2], left_inv := , right_inv := }
Instances For
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
• = { toFun := i.insertNth none some, invFun := fun (x : Option (Fin n)) => x.casesOn' i i.succAbove, left_inv := , right_inv := }
Instances For
@[simp]
theorem finSuccEquiv'_at {n : } (i : Fin (n + 1)) :
() i = none
@[simp]
theorem finSuccEquiv'_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
() (i.succAbove j) = some j
theorem finSuccEquiv'_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
() m.castSucc = some m
theorem finSuccEquiv'_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
() m.succ = some m
@[simp]
theorem finSuccEquiv'_symm_none {n : } (i : Fin (n + 1)) :
().symm none = i
@[simp]
theorem finSuccEquiv'_symm_some {n : } (i : Fin (n + 1)) (j : Fin n) :
().symm (some j) = i.succAbove j
theorem finSuccEquiv'_symm_some_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
().symm (some m) = m.castSucc
theorem finSuccEquiv'_symm_some_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
().symm (some m) = m.succ
theorem finSuccEquiv'_symm_coe_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : m.castSucc < i) :
().symm (some m) = m.castSucc
theorem finSuccEquiv'_symm_coe_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i m.castSucc) :
().symm (some m) = m.succ
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
Instances For
@[simp]
theorem finSuccEquiv_zero {n : } :
() 0 = none
@[simp]
theorem finSuccEquiv_succ {n : } (m : Fin n) :
() m.succ = some m
@[simp]
theorem finSuccEquiv_symm_none {n : } :
().symm none = 0
@[simp]
theorem finSuccEquiv_symm_some {n : } (m : Fin n) :
().symm (some m) = m.succ
theorem finSuccEquiv'_zero {n : } :

The equiv version of Fin.predAbove_zero.

theorem finSuccEquiv'_last_apply_castSucc {n : } (i : Fin n) :
() i.castSucc = some i
theorem finSuccEquiv'_last_apply {n : } {i : Fin (n + 1)} (h : i ) :
() i = some (i.castLT )
theorem finSuccEquiv'_ne_last_apply {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (hi : i ) (hj : j i) :
() j = some ((i.castLT ).predAbove j)
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
• = ().symm,
Instances For
theorem finSuccAboveEquiv_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
i = p.succAbove i,
theorem finSuccAboveEquiv_symm_apply_last {n : } (x : { x : Fin (n + 1) // x }) :
().symm x = (x).castLT
theorem finSuccAboveEquiv_symm_apply_ne_last {n : } {p : Fin (n + 1)} (h : p ) (x : { x : Fin (n + 1) // x p }) :
.symm x = (p.castLT ).predAbove 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

Equations
• finSuccEquivLast =
Instances For
@[simp]
theorem finSuccEquivLast_castSucc {n : } (i : Fin n) :
finSuccEquivLast i.castSucc = some i
@[simp]
theorem finSuccEquivLast_last {n : } :
finSuccEquivLast () = none
@[simp]
theorem finSuccEquivLast_symm_some {n : } (i : Fin n) :
finSuccEquivLast.symm (some i) = i.castSucc
@[simp]
theorem finSuccEquivLast_symm_none {n : } :
finSuccEquivLast.symm none =
@[simp]
theorem Equiv.piFinSuccAbove_apply {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
() = fun (f : (j : Fin (n + 1)) → α j) => (f i, i.removeNth f)
@[simp]
theorem Equiv.piFinSuccAbove_symm_apply {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
().symm = fun (f : α i × ((j : Fin n) → α (i.succAbove j))) => i.insertNth f.1 f.2
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.
Instances For
@[simp]
theorem Equiv.piFinSucc_apply (n : ) (β : Type u) :
() = fun (f : Fin (n + 1)β) => (f 0, )
@[simp]
theorem Equiv.piFinSucc_symm_apply (n : ) (β : Type u) :
().symm = fun (f : β × (Fin nβ)) => Fin.cons f.1 f.2
def Equiv.piFinSucc (n : ) (β : Type u) :
(Fin (n + 1)β) β × (Fin nβ)

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

Equations
Instances For
def Equiv.embeddingFinSucc (n : ) (ι : Type u_1) :
(Fin (n + 1) ι) (e : Fin n ι) × { i : ι // i }

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
• = (().embeddingCongr ()).trans
Instances For
@[simp]
theorem Equiv.embeddingFinSucc_fst {n : } {ι : Type u_1} (e : Fin (n + 1) ι) :
(() e).fst = e Fin.succ
@[simp]
theorem Equiv.embeddingFinSucc_snd {n : } {ι : Type u_1} (e : Fin (n + 1) ι) :
(() e).snd = e 0
@[simp]
theorem Equiv.coe_embeddingFinSucc_symm {n : } {ι : Type u_1} (f : (e : Fin n ι) × { i : ι // i }) :
(().symm f) = Fin.cons f.snd f.fst
@[simp]
theorem Equiv.piFinCastSucc_symm_apply (n : ) (β : Type u) :
().symm = fun (f : β × (Fin nβ)) => Fin.snoc f.2 f.1
@[simp]
theorem Equiv.piFinCastSucc_apply (n : ) (β : Type u) :
() = fun (f : Fin (n + 1)β) => (f (), )
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
Instances For
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 () (), invFun := fun (i : Fin (m + n)) => Fin.addCases Sum.inl Sum.inr i, left_inv := , right_inv := }
Instances For
@[simp]
theorem finSumFinEquiv_apply_left {m : } {n : } (i : Fin m) :
finSumFinEquiv () =
@[simp]
theorem finSumFinEquiv_apply_right {m : } {n : } (i : Fin n) :
finSumFinEquiv () =
@[simp]
theorem finSumFinEquiv_symm_apply_castAdd {m : } {n : } (x : Fin m) :
finSumFinEquiv.symm () =
@[simp]
theorem finSumFinEquiv_symm_apply_natAdd {m : } {n : } (x : Fin n) :
finSumFinEquiv.symm () =
@[simp]
theorem finSumFinEquiv_symm_last {n : } :
finSumFinEquiv.symm () =
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
Instances For
@[simp]
theorem finAddFlip_apply_castAdd {m : } (k : Fin m) (n : ) :
@[simp]
theorem finAddFlip_apply_natAdd {n : } (k : Fin n) (m : ) :
@[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
@[simp]
theorem finAddFlip_apply_mk_right {m : } {n : } {k : } (h₁ : m k) (h₂ : k < m + n) :
finAddFlip k, h₂ = k - m,
def finRotate (n : ) :

Rotate Fin n one step to the right.

Equations
• = match x with | 0 => Equiv.refl (Fin 0) | n.succ => finAddFlip.trans ()
Instances For
@[simp]
theorem finRotate_succ (n : ) :
finRotate (n + 1) = finAddFlip.trans ()
theorem finRotate_of_lt {n : } {k : } (h : k < n) :
(finRotate (n + 1)) k, = k + 1,
theorem finRotate_last' {n : } :
(finRotate (n + 1)) n, = 0,
theorem finRotate_last {n : } :
(finRotate (n + 1)) () = 0
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)
@[simp]
@[simp]
theorem finRotate_succ_apply {n : } (i : Fin (n + 1)) :
(finRotate (n + 1)) i = i + 1
theorem finRotate_apply_zero {n : } :
(finRotate n.succ) 0 = 1
theorem coe_finRotate_of_ne_last {n : } {i : Fin n.succ} (h : i ) :
((finRotate (n + 1)) i) = i + 1
theorem coe_finRotate {n : } (i : Fin n.succ) :
((finRotate n.succ) i) = if i = then 0 else i + 1
@[simp]
theorem finProdFinEquiv_symm_apply {m : } {n : } (x : Fin (m * n)) :
finProdFinEquiv.symm x = (x.divNat, x.modNat)
@[simp]
theorem finProdFinEquiv_apply_val {m : } {n : } (x : Fin m × Fin n) :
(finProdFinEquiv x) = x.2 + n * x.1
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
@[simp]
theorem Nat.divModEquiv_apply (n : ) [] (a : ) :
n.divModEquiv a = (a / n, a)
@[simp]
theorem Nat.divModEquiv_symm_apply (n : ) [] (p : × Fin n) :
n.divModEquiv.symm p = p.1 * n + p.2
def Nat.divModEquiv (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 := }
Instances For
@[simp]
theorem Int.divModEquiv_apply (n : ) [] (a : ) :
() a = (a / n, (a.natMod n))
@[simp]
theorem Int.divModEquiv_symm_apply (n : ) [] (p : × Fin n) :
().symm p = p.1 * n + p.2
def Int.divModEquiv (n : ) [] :

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

Equations
• = { toFun := fun (a : ) => (a / n, (a.natMod n)), invFun := fun (p : × Fin n) => p.1 * n + p.2, left_inv := , right_inv := }
Instances For
@[simp]
theorem Fin.castLEquiv_symm_apply {n : } {m : } (h : n m) (i : { i : Fin m // i < n }) :
().symm i = i,
@[simp]
theorem Fin.castLEquiv_apply {n : } {m : } (h : n m) (i : Fin n) :
() i = ,
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
• = { toFun := fun (i : Fin n) => ⟨, , invFun := fun (i : { i : Fin m // i < n }) => i, , left_inv := , right_inv := }
Instances For

Fin 0 is a subsingleton.

Equations

Fin 1 is a subsingleton.

Equations