Documentation

Mathlib.Logic.Equiv.Fin

Equivalences for Fin n #

Equivalence between Fin 0 and Empty.

Equations

Equivalence between Fin 0 and PEmpty.

Equations

Equivalence between Fin 1 and Unit.

Equations

Equivalence between Fin 2 and Bool.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem piFinTwoEquiv_symm_apply (α : Fin 2Type u) :
↑(Equiv.symm (piFinTwoEquiv α)) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)
@[simp]
theorem piFinTwoEquiv_apply (α : Fin 2Type u) :
↑(piFinTwoEquiv α) = fun f => (f 0, f 1)
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
  • One or more equations did not get rendered due to their size.
theorem Fin.preimage_apply_01_prod {α : Fin 2Type 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 (Matrix.vecCons s (Matrix.vecCons t Matrix.vecEmpty))
@[simp]
theorem prodEquivPiFinTwo_symm_apply (α : Type u) (β : Type u) :
↑(Equiv.symm (prodEquivPiFinTwo α β)) = 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 α (Matrix.vecCons β Matrix.vecEmpty) 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
@[simp]
theorem finTwoArrowEquiv_symm_apply (α : Type u_1) :
↑(Equiv.symm (finTwoArrowEquiv α)) = fun x => Matrix.vecCons x.fst (Matrix.vecCons x.snd Matrix.vecEmpty)
@[simp]
theorem finTwoArrowEquiv_apply (α : Type u_1) :
↑(finTwoArrowEquiv α) = (piFinTwoEquiv fun x => α).toFun
def finTwoArrowEquiv (α : Type u_1) :
(Fin 2α) α × α

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

Equations
  • One or more equations did not get rendered due to their size.
def OrderIso.piFinTwoIso (α : Fin 2Type u) [inst : (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.

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

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

Equations
  • One or more equations did not get rendered due to their size.
def finCongr {m : } {n : } (h : m = n) :
Fin m Fin n

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

Equations
@[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) :
@[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) :
↑(↑(Equiv.symm (finCongr h)) 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.

Equations
  • One or more equations did not get rendered due to their size.
@[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).toEmbedding j) = some j
theorem finSuccEquiv'_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc.toEmbedding m < i) :
↑(finSuccEquiv' i) (Fin.castSucc.toEmbedding m) = some m
theorem finSuccEquiv'_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i Fin.castSucc.toEmbedding m) :
@[simp]
theorem finSuccEquiv'_symm_none {n : } (i : Fin (n + 1)) :
↑(Equiv.symm (finSuccEquiv' i)) none = i
@[simp]
theorem finSuccEquiv'_symm_some {n : } (i : Fin (n + 1)) (j : Fin n) :
↑(Equiv.symm (finSuccEquiv' i)) (some j) = (Fin.succAbove i).toEmbedding j
theorem finSuccEquiv'_symm_some_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc.toEmbedding m < i) :
↑(Equiv.symm (finSuccEquiv' i)) (some m) = Fin.castSucc.toEmbedding m
theorem finSuccEquiv'_symm_some_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i Fin.castSucc.toEmbedding m) :
theorem finSuccEquiv'_symm_coe_below {n : } {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc.toEmbedding m < i) :
↑(Equiv.symm (finSuccEquiv' i)) (some m) = Fin.castSucc.toEmbedding m
theorem finSuccEquiv'_symm_coe_above {n : } {i : Fin (n + 1)} {m : Fin n} (h : i Fin.castSucc.toEmbedding 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.

Equations
@[simp]
theorem finSuccEquiv_zero {n : } :
↑(finSuccEquiv n) 0 = none
@[simp]
theorem finSuccEquiv_succ {n : } (m : Fin n) :
@[simp]
theorem finSuccEquiv_symm_none {n : } :
↑(Equiv.symm (finSuccEquiv n)) none = 0
@[simp]
theorem finSuccEquiv_symm_some {n : } (m : Fin n) :
theorem finSuccEquiv'_last_apply_castSucc {n : } (i : Fin n) :
↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc.toEmbedding 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}.

Equations
  • One or more equations did not get rendered due to their size.
theorem finSuccAboveEquiv_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
(RelIso.toRelEmbedding (finSuccAboveEquiv p)).toEmbedding i = { val := (Fin.succAbove p).toEmbedding i, property := (_ : (Fin.succAbove p).toEmbedding i p) }
theorem finSuccAboveEquiv_symm_apply_last {n : } (x : { x // x Fin.last n }) :
(RelIso.toRelEmbedding (OrderIso.symm (finSuccAboveEquiv (Fin.last n)))).toEmbedding 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 }) :
(RelIso.toRelEmbedding (OrderIso.symm (finSuccAboveEquiv p))).toEmbedding 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

Equations
@[simp]
theorem finSuccEquivLast_castSucc {n : } (i : Fin n) :
finSuccEquivLast (Fin.castSucc.toEmbedding i) = some i
@[simp]
theorem finSuccEquivLast_last {n : } :
finSuccEquivLast (Fin.last n) = none
@[simp]
theorem finSuccEquivLast_symm_some {n : } (i : Fin n) :
↑(Equiv.symm finSuccEquivLast) (some i) = Fin.castSucc.toEmbedding i
@[simp]
theorem finSuccEquivLast_symm_none {n : } :
↑(Equiv.symm finSuccEquivLast) none = Fin.last n
@[simp]
theorem Equiv.piFinSuccAboveEquiv_symm_apply {n : } (α : Fin (n + 1)Type u) (i : Fin (n + 1)) :
↑(Equiv.symm (Equiv.piFinSuccAboveEquiv α i)) = fun f => Fin.insertNth i f.fst f.snd
@[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).toEmbedding j))
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).toEmbedding 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.
def OrderIso.piFinSuccAboveIso {n : } (α : Fin (n + 1)Type u) [inst : (i : Fin (n + 1)) → LE (α i)] (i : Fin (n + 1)) :
((j : Fin (n + 1)) → α j) ≃o α i × ((j : Fin n) → α ((Fin.succAbove i).toEmbedding j))

Order isomorphism 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.
@[simp]
theorem Equiv.piFinSucc_symm_apply (n : ) (β : Type u) :
↑(Equiv.symm (Equiv.piFinSucc n β)) = fun f => Fin.cons f.fst f.snd
@[simp]
theorem Equiv.piFinSucc_apply (n : ) (β : Type u) :
↑(Equiv.piFinSucc n β) = fun f => (f 0, fun j => f (Fin.succ j))
def Equiv.piFinSucc (n : ) (β : Type u) :
(Fin (n + 1)β) β × (Fin nβ)

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

Equations
def finSumFinEquiv {m : } {n : } :
Fin m Fin n Fin (m + n)

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem finSumFinEquiv_apply_left {m : } {n : } (i : Fin m) :
finSumFinEquiv (Sum.inl i) = (Fin.castAdd n).toEmbedding i
@[simp]
theorem finSumFinEquiv_apply_right {m : } {n : } (i : Fin n) :
finSumFinEquiv (Sum.inr i) = (Fin.natAdd m).toEmbedding i
@[simp]
theorem finSumFinEquiv_symm_apply_castAdd {m : } {n : } (x : Fin m) :
↑(Equiv.symm finSumFinEquiv) ((Fin.castAdd n).toEmbedding x) = Sum.inl x
@[simp]
theorem finSumFinEquiv_symm_apply_natAdd {m : } {n : } (x : Fin n) :
↑(Equiv.symm finSumFinEquiv) ((Fin.natAdd m).toEmbedding x) = Sum.inr x
@[simp]
theorem finSumFinEquiv_symm_last {n : } :
↑(Equiv.symm finSumFinEquiv) (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.

Equations
@[simp]
theorem finAddFlip_apply_castAdd {m : } (k : Fin m) (n : ) :
finAddFlip ((Fin.castAdd n).toEmbedding k) = (Fin.natAdd n).toEmbedding k
@[simp]
theorem finAddFlip_apply_natAdd {n : } (k : Fin n) (m : ) :
finAddFlip ((Fin.natAdd m).toEmbedding k) = (Fin.castAdd m).toEmbedding 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 : ) :

Rotate Fin n one step to the right.

Equations
theorem finRotate_succ (n : ) :
finRotate (n + 1) = Equiv.trans finAddFlip (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_succ_apply {n : } (i : Fin (n + 1)) :
↑(finRotate (n + 1)) i = i + 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_apply_val {m : } {n : } (x : Fin m × Fin n) :
↑(finProdFinEquiv x) = x.snd + n * x.fst
@[simp]
theorem finProdFinEquiv_symm_apply {m : } {n : } (x : Fin (m * n)) :
↑(Equiv.symm finProdFinEquiv) x = (Fin.divNat x, Fin.modNat x)
def finProdFinEquiv {m : } {n : } :
Fin m × Fin n Fin (m * n)

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Nat.divModEquiv_symm_apply (n : ) [inst : NeZero n] (p : × Fin n) :
↑(Equiv.symm (Nat.divModEquiv n)) p = p.fst * n + p.snd
@[simp]
theorem Nat.divModEquiv_apply (n : ) [inst : NeZero n] (a : ) :
↑(Nat.divModEquiv n) a = (a / n, a)
def Nat.divModEquiv (n : ) [inst : NeZero 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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Int.divModEquiv_symm_apply (n : ) [inst : NeZero n] (p : × Fin n) :
↑(Equiv.symm (Int.divModEquiv n)) p = p.fst * n + p.snd
@[simp]
theorem Int.divModEquiv_apply (n : ) [inst : NeZero n] (a : ) :
↑(Int.divModEquiv n) a = (a / n, ↑(Int.natMod a n))
def Int.divModEquiv (n : ) [inst : NeZero n] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.castLeOrderIso_apply {n : } {m : } (h : n m) (i : Fin n) :
(RelIso.toRelEmbedding (Fin.castLeOrderIso h)).toEmbedding i = { val := (Fin.castLe h).toEmbedding i, property := (_ : i < n) }
@[simp]
theorem Fin.castLeOrderIso_symm_apply {n : } {m : } (h : n m) (i : { i // i < n }) :
(RelIso.toRelEmbedding (RelIso.symm (Fin.castLeOrderIso h))).toEmbedding i = { val := i, isLt := (_ : 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.

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