Mathlib.Logic.Equiv.Fin.Basic

Fin.preimage_apply_01_prod theorem

 {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) :
  (fun f : ∀ i, α i => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (Fin.cons s <| Fin.cons t finZeroElim)

Full source

theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) :
    (fun f : ∀ i, α i => (f 0, f 1)) ⁻¹' s ×ˢ t =
      Set.pi Set.univ (Fin.cons s <| Fin.cons t finZeroElim) := by
  ext f
  simp [Fin.forall_fin_two]

Preimage of Product Set under Evaluation Map for `Fin 2` Functions

Informal description

For any family of types $\alpha : \text{Fin}\,2 \to \text{Type}$ and subsets $s \subseteq \alpha(0)$, $t \subseteq \alpha(1)$, the preimage of the product set $s \times t$ under the evaluation map $(f \mapsto (f(0), f(1)))$ is equal to the dependent product $\prod_{i \in \text{Fin}\,2} \beta(i)$, where $\beta$ is the family $\text{Fin.cons}\,s\,(\text{Fin.cons}\,t\,\text{finZeroElim})$.

Fin.preimage_apply_01_prod' theorem

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

Full source

theorem Fin.preimage_apply_01_prod' {α : Type u} (s t : Set α) :
    (fun f : Fin 2 → α => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ ![s, t] :=
  @Fin.preimage_apply_01_prod (fun _ => α) s t

Preimage of Product Set under Evaluation Map for Functions on `Fin 2` (Non-Dependent Case)

Informal description

For any type $\alpha$ and subsets $s, t \subseteq \alpha$, the preimage of the product set $s \times t$ under the evaluation map $(f \mapsto (f(0), f(1)))$ for functions $f : \text{Fin}\,2 \to \alpha$ is equal to the dependent product $\prod_{i \in \text{Fin}\,2} \gamma(i)$, where $\gamma$ is the vector $\text{![s, t]}$.

prodEquivPiFinTwo definition

(α β : Type u) : α × β ≃ ∀ i : Fin 2, ![α, β] i

Full source

/-- A product space `α × β` is equivalent to the space `Π i : Fin 2, γ i`, where
`γ = Fin.cons α (Fin.cons β finZeroElim)`. See also `piFinTwoEquiv` and
`finTwoArrowEquiv`. -/
@[simps! -fullyApplied]
def prodEquivPiFinTwo (α β : Type u) : α × βα × β ≃ ∀ i : Fin 2, ![α, β] i :=
  (piFinTwoEquiv (Fin.cons α (Fin.cons β finZeroElim))).symm

Equivalence between pairs and dependent functions on `Fin 2`

Informal description

The equivalence `prodEquivPiFinTwo` establishes a bijection between the Cartesian product $\alpha \times \beta$ and the space of dependent functions $\Pi i : \text{Fin}\,2, \gamma i$, where $\gamma$ is the family $\text{Fin.cons}\,\alpha\,(\text{Fin.cons}\,\beta\,\text{finZeroElim})$. Specifically: - The forward direction maps a pair $(x, y) \in \alpha \times \beta$ to the dependent function $f$ where $f(0) = x$ and $f(1) = y$. - The backward direction reconstructs the pair from a dependent function $f$ by taking $(f(0), f(1))$. This equivalence is the inverse of `piFinTwoEquiv` applied to the family $\gamma = \text{Fin.cons}\,\alpha\,(\text{Fin.cons}\,\beta\,\text{finZeroElim})$.

finTwoArrowEquiv definition

(α : Type*) : (Fin 2 → α) ≃ α × α

Full source

/-- The space of functions `Fin 2 → α` is equivalent to `α × α`. See also `piFinTwoEquiv` and
`prodEquivPiFinTwo`. -/
@[simps -fullyApplied]
def finTwoArrowEquiv (α : Type*) : (Fin 2 → α) ≃ α × α :=
  { piFinTwoEquiv fun _ => α with invFun := fun x => ![x.1, x.2] }

Equivalence between functions on `Fin 2` and pairs in `α × α`

Informal description

The equivalence `finTwoArrowEquiv` establishes a bijection between the space of functions from `Fin 2` to a type `α` and the Cartesian product `α × α`. Specifically: - The forward direction maps a function `f : Fin 2 → α` to the pair `(f 0, f 1)`. - The backward direction maps a pair `(x, y)` to the function `Fin.cons x (Fin.cons y finZeroElim)`.

finSuccEquiv' definition

(i : Fin (n + 1)) : Fin (n + 1) ≃ Option (Fin n)

Full source

/-- 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`. -/
def finSuccEquiv' (i : Fin (n + 1)) : FinFin (n + 1) ≃ Option (Fin n) where
  toFun := i.insertNth none some
  invFun x := x.casesOn' i (Fin.succAbove i)
  left_inv x := Fin.succAboveCases i (by simp) (fun j => by simp) x
  right_inv x := by cases x <;> dsimp <;> simp

Equivalence between $\text{Fin}(n+1)$ and $\text{Option}\,(\text{Fin}\,n)$ with a hole at $i$

Informal description

For a given index $i \in \text{Fin}(n+1)$, the equivalence $\text{finSuccEquiv'}\,i$ maps elements of $\text{Fin}(n+1)$ to $\text{Option}\,(\text{Fin}\,n)$ by: - Sending $i$ to $\text{none}$. - For other elements $j \neq i$, it sends $j$ to $\text{some}\,k$, where $k$ is the corresponding element in $\text{Fin}\,n$ obtained via the $\text{succAbove}$ operation. The inverse operation reconstructs the original element by: - Mapping $\text{none}$ back to $i$. - Mapping $\text{some}\,k$ to the element obtained by applying $\text{succAbove}\,i$ to $k$. This equivalence effectively removes the element $i$ from $\text{Fin}(n+1)$ and shifts the remaining elements to $\text{Fin}\,n$, with $i$ represented as $\text{none}$.

finSuccEquiv'_at theorem

(i : Fin (n + 1)) : (finSuccEquiv' i) i = none

Full source

@[simp]
theorem finSuccEquiv'_at (i : Fin (n + 1)) : (finSuccEquiv' i) i = none := by
  simp [finSuccEquiv']

Mapping of Pivot Index to None in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

For any index $i \in \text{Fin}(n+1)$, the equivalence $\text{finSuccEquiv'}\,i$ maps $i$ to $\text{none}$.

finSuccEquiv'_succAbove theorem

(i : Fin (n + 1)) (j : Fin n) : finSuccEquiv' i (i.succAbove j) = some j

Full source

@[simp]
theorem finSuccEquiv'_succAbove (i : Fin (n + 1)) (j : Fin n) :
    finSuccEquiv' i (i.succAbove j) = some j :=
  @Fin.insertNth_apply_succAbove n (fun _ => Option (Fin n)) i _ _ _

Mapping of Shifted Index to Some in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

For any index $i \in \text{Fin}(n+1)$ and any $j \in \text{Fin}(n)$, the equivalence $\text{finSuccEquiv'}\,i$ maps the element $i.\text{succAbove}\,j$ of $\text{Fin}(n+1)$ to $\text{some}\,j$ in $\text{Option}\,(\text{Fin}\,n)$.

finSuccEquiv'_below theorem

{i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : (finSuccEquiv' i) (Fin.castSucc m) = m

Full source

theorem finSuccEquiv'_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i) (Fin.castSucc m) = m := by
  rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]

Mapping of Cast Index Below Hole to Original Index in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

For any index $i \in \text{Fin}(n+1)$ and any $m \in \text{Fin}(n)$, if the cast of $m$ to $\text{Fin}(n+1)$ (denoted as $\text{castSucc}\,m$) is strictly less than $i$, then the equivalence $\text{finSuccEquiv'}\,i$ maps $\text{castSucc}\,m$ to $m$.

finSuccEquiv'_above theorem

{i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : (finSuccEquiv' i) m.succ = some m

Full source

theorem finSuccEquiv'_above {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) :
    (finSuccEquiv' i) m.succ = some m := by
  rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]

Mapping of Successor to Some in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$ When Below Index

Informal description

For any index $i \in \text{Fin}(n+1)$ and any $m \in \text{Fin}(n)$, if $i \leq \text{castSucc}(m)$, then the equivalence $\text{finSuccEquiv'}\,i$ maps the successor of $m$ to $\text{some}\,m$ in $\text{Option}\,(\text{Fin}\,n)$.

finSuccEquiv'_symm_none theorem

(i : Fin (n + 1)) : (finSuccEquiv' i).symm none = i

Full source

@[simp]
theorem finSuccEquiv'_symm_none (i : Fin (n + 1)) : (finSuccEquiv' i).symm none = i :=
  rfl

Inverse of $\text{finSuccEquiv'}$ maps $\text{none}$ to the hole index $i$

Informal description

For any element $i \in \text{Fin}(n+1)$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $\text{none}$ back to $i$. That is, $(\text{finSuccEquiv'}\,i)^{-1}(\text{none}) = i$.

finSuccEquiv'_symm_some theorem

(i : Fin (n + 1)) (j : Fin n) : (finSuccEquiv' i).symm (some j) = i.succAbove j

Full source

@[simp]
theorem finSuccEquiv'_symm_some (i : Fin (n + 1)) (j : Fin n) :
    (finSuccEquiv' i).symm (some j) = i.succAbove j :=
  rfl

Inverse of $\text{finSuccEquiv'}$ Maps $\text{some}\,j$ to $\text{succAbove}\,i\,j$

Informal description

For any element $i \in \text{Fin}(n+1)$ and any $j \in \text{Fin}(n)$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $\text{some}\,j$ to the element obtained by applying the $\text{succAbove}$ operation to $i$ and $j$. That is, $(\text{finSuccEquiv'}\,i)^{-1}(\text{some}\,j) = i.\text{succAbove}\,j$.

finSuccEquiv'_eq_some theorem

{i j : Fin (n + 1)} {k : Fin n} : finSuccEquiv' i j = k ↔ j = i.succAbove k

Full source

@[simp]
theorem finSuccEquiv'_eq_some {i j : Fin (n + 1)} {k : Fin n} :
    finSuccEquiv'finSuccEquiv' i j = k ↔ j = i.succAbove k :=
  (finSuccEquiv' i).apply_eq_iff_eq_symm_apply

Characterization of $\text{finSuccEquiv'}$ via $\text{succAbove}$

Informal description

For any elements $i, j \in \text{Fin}(n+1)$ and $k \in \text{Fin}(n)$, the equivalence $\text{finSuccEquiv'}\,i$ maps $j$ to $\text{some}\,k$ if and only if $j$ is equal to the embedding of $k$ via $\text{succAbove}\,i$. That is, $\text{finSuccEquiv'}\,i\,j = \text{some}\,k \leftrightarrow j = i.\text{succAbove}\,k$.

finSuccEquiv'_eq_none theorem

{i j : Fin (n + 1)} : finSuccEquiv' i j = none ↔ i = j

Full source

@[simp]
theorem finSuccEquiv'_eq_none {i j : Fin (n + 1)} : finSuccEquiv'finSuccEquiv' i j = none ↔ i = j :=
  (finSuccEquiv' i).apply_eq_iff_eq_symm_apply.trans eq_comm

Characterization of $\text{finSuccEquiv'}$ Mapping to $\text{none}$

Informal description

For any elements $i, j \in \text{Fin}(n+1)$, the equivalence $\text{finSuccEquiv'}\,i$ maps $j$ to $\text{none}$ if and only if $i = j$.

finSuccEquiv'_symm_some_below theorem

{i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : (finSuccEquiv' i).symm (some m) = Fin.castSucc m

Full source

theorem finSuccEquiv'_symm_some_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i).symm (some m) = Fin.castSucc m :=
  Fin.succAbove_of_castSucc_lt i m h

Inverse of $\text{finSuccEquiv'}$ maps $\text{some}\,m$ to $\text{castSucc}\,m$ when $\text{castSucc}\,m < i$

Informal description

For any natural number $n$, given an element $i \in \text{Fin}(n+1)$ and an element $m \in \text{Fin}(n)$ such that the cast of $m$ to $\text{Fin}(n+1)$ (denoted as $\text{castSucc}\,m$) is strictly less than $i$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $\text{some}\,m$ to $\text{castSucc}\,m$.

finSuccEquiv'_symm_some_above theorem

{i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : (finSuccEquiv' i).symm (some m) = m.succ

Full source

theorem finSuccEquiv'_symm_some_above {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) :
    (finSuccEquiv' i).symm (some m) = m.succ :=
  Fin.succAbove_of_le_castSucc i m h

Inverse of $\text{finSuccEquiv'}$ maps $\text{some}\,m$ to $\text{succ}(m)$ when $i \leq \text{castSucc}(m)$

Informal description

For any natural number $n$, given an element $i \in \text{Fin}(n+1)$ and an element $m \in \text{Fin}(n)$ such that $i \leq \text{castSucc}(m)$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $\text{some}\,m$ to the successor of $m$, i.e., $\text{succ}(m)$.

finSuccEquiv'_symm_coe_below theorem

{i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) : (finSuccEquiv' i).symm m = Fin.castSucc m

Full source

theorem finSuccEquiv'_symm_coe_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i).symm m = Fin.castSucc m :=
  finSuccEquiv'_symm_some_below h

Inverse of $\text{finSuccEquiv'}$ maps $m$ to $\text{castSucc}\,m$ when $\text{castSucc}\,m < i$

Informal description

For any natural number $n$, given an element $i \in \text{Fin}(n+1)$ and an element $m \in \text{Fin}(n)$ such that the cast of $m$ to $\text{Fin}(n+1)$ (denoted as $\text{castSucc}\,m$) is strictly less than $i$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $m$ to $\text{castSucc}\,m$.

finSuccEquiv'_symm_coe_above theorem

{i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) : (finSuccEquiv' i).symm m = m.succ

Full source

theorem finSuccEquiv'_symm_coe_above {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) :
    (finSuccEquiv' i).symm m = m.succ :=
  finSuccEquiv'_symm_some_above h

Inverse of $\text{finSuccEquiv'}$ maps $m$ to $\text{succ}(m)$ when $i \leq \text{castSucc}(m)$

Informal description

For any natural number $n$, given an element $i \in \text{Fin}(n+1)$ and an element $m \in \text{Fin}(n)$ such that $i \leq \text{castSucc}(m)$, the inverse of the equivalence $\text{finSuccEquiv'}\,i$ maps $m$ to the successor of $m$, i.e., $\text{succ}(m)$.

finSuccEquiv definition

(n : ℕ) : Fin (n + 1) ≃ Option (Fin n)

Full source

/-- 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`. -/
def finSuccEquiv (n : ℕ) : FinFin (n + 1) ≃ Option (Fin n) :=
  finSuccEquiv' 0

Equivalence between $\text{Fin}(n+1)$ and $\text{Option}\,(\text{Fin}\,n)$ with zero mapped to none

Informal description

The equivalence between the finite type $\text{Fin}(n+1)$ and $\text{Option}\,(\text{Fin}\,n)$ maps: - The element $0 \in \text{Fin}(n+1)$ to $\text{none}$. - The element $m.\text{succ} \in \text{Fin}(n+1)$ to $\text{some}\,m$ for any $m \in \text{Fin}\,n$. This equivalence effectively removes the zero element from $\text{Fin}(n+1)$ and shifts the remaining elements to $\text{Fin}\,n$, with zero represented as $\text{none}$.

finSuccEquiv_zero theorem

: (finSuccEquiv n) 0 = none

Full source

@[simp]
theorem finSuccEquiv_zero : (finSuccEquiv n) 0 = none :=
  rfl

Zero maps to none under $\text{finSuccEquiv}$

Informal description

For any natural number $n$, the equivalence $\text{finSuccEquiv}\,n$ maps the zero element of $\text{Fin}(n+1)$ to $\text{none}$ in $\text{Option}\,(\text{Fin}\,n)$, i.e., $\text{finSuccEquiv}\,n\,0 = \text{none}$.

finSuccEquiv_succ theorem

(m : Fin n) : (finSuccEquiv n) m.succ = some m

Full source

@[simp]
theorem finSuccEquiv_succ (m : Fin n) : (finSuccEquiv n) m.succ = some m :=
  finSuccEquiv'_above (Fin.zero_le _)

Successor Mapping in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

For any element $m$ in the finite type $\text{Fin}\,n$, the equivalence $\text{finSuccEquiv}\,n$ maps the successor of $m$ in $\text{Fin}(n+1)$ to $\text{some}\,m$ in $\text{Option}\,(\text{Fin}\,n)$, i.e., $\text{finSuccEquiv}\,n\,(m.\text{succ}) = \text{some}\,m$.

finSuccEquiv_symm_none theorem

: (finSuccEquiv n).symm none = 0

Full source

@[simp]
theorem finSuccEquiv_symm_none : (finSuccEquiv n).symm none = 0 :=
  finSuccEquiv'_symm_none _

Inverse of $\text{finSuccEquiv}$ Maps None to Zero

Informal description

The inverse of the equivalence $\text{finSuccEquiv}\,n$ maps $\text{none}$ back to the zero element of $\text{Fin}(n+1)$, i.e., $(\text{finSuccEquiv}\,n)^{-1}(\text{none}) = 0$.

finSuccEquiv_symm_some theorem

(m : Fin n) : (finSuccEquiv n).symm (some m) = m.succ

Full source

@[simp]
theorem finSuccEquiv_symm_some (m : Fin n) : (finSuccEquiv n).symm (some m) = m.succ :=
  congr_fun Fin.succAbove_zero m

Inverse of $\text{finSuccEquiv}$ Maps Some to Successor

Informal description

For any element $m$ in the finite type $\text{Fin}\,n$, the inverse of the equivalence $\text{finSuccEquiv}\,n$ maps $\text{some}\,m$ to the successor of $m$ in $\text{Fin}(n+1)$, i.e., $(\text{finSuccEquiv}\,n)^{-1}(\text{some}\,m) = m.\text{succ}$.

finSuccEquiv_eq_some theorem

{i : Fin (n + 1)} {j : Fin n} : finSuccEquiv n i = j ↔ i = j.succ

Full source

@[simp]
theorem finSuccEquiv_eq_some {i : Fin (n + 1)} {j : Fin n} :
    finSuccEquivfinSuccEquiv n i = j ↔ i = j.succ :=
  (finSuccEquiv n).apply_eq_iff_eq_symm_apply

Characterization of Successor via $\text{finSuccEquiv}$: $\text{finSuccEquiv}\,n\,i = \text{some}\,j \leftrightarrow i = j.\text{succ}$

Informal description

For any element $i \in \text{Fin}(n+1)$ and $j \in \text{Fin}(n)$, the equivalence $\text{finSuccEquiv}\,n$ maps $i$ to $\text{some}\,j$ if and only if $i$ is the successor of $j$ in $\text{Fin}(n+1)$, i.e., $\text{finSuccEquiv}\,n\,i = \text{some}\,j \leftrightarrow i = j.\text{succ}$.

finSuccEquiv_eq_none theorem

{i : Fin (n + 1)} : finSuccEquiv n i = none ↔ i = 0

Full source

@[simp]
theorem finSuccEquiv_eq_none {i : Fin (n + 1)} : finSuccEquivfinSuccEquiv n i = none ↔ i = 0 :=
  (finSuccEquiv n).apply_eq_iff_eq_symm_apply

Characterization of Zero via $\text{finSuccEquiv}$: $\text{finSuccEquiv}\,n\,i = \text{none} \leftrightarrow i = 0$

Informal description

For any element $i$ in the finite type $\text{Fin}(n+1)$, the equivalence $\text{finSuccEquiv}\,n$ maps $i$ to $\text{none}$ if and only if $i = 0$.

finSuccEquiv'_zero theorem

: finSuccEquiv' (0 : Fin (n + 1)) = finSuccEquiv n

Full source

/-- The equiv version of `Fin.predAbove_zero`. -/
theorem finSuccEquiv'_zero : finSuccEquiv' (0 : Fin (n + 1)) = finSuccEquiv n :=
  rfl

Equivalence at Zero is $\text{finSuccEquiv}$

Informal description

The equivalence $\text{finSuccEquiv'}$ evaluated at the zero element of $\text{Fin}(n+1)$ is equal to the equivalence $\text{finSuccEquiv}\,n$. That is, $\text{finSuccEquiv'}\,0 = \text{finSuccEquiv}\,n$.

finSuccEquiv'_last_apply_castSucc theorem

(i : Fin n) : finSuccEquiv' (Fin.last n) (Fin.castSucc i) = i

Full source

theorem finSuccEquiv'_last_apply_castSucc (i : Fin n) :
    finSuccEquiv' (Fin.last n) (Fin.castSucc i) = i := by
  rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]

Equivalence at Last Element Maps Cast Embedding to Original Element

Informal description

For any element $i$ of the finite type $\text{Fin}(n)$, the equivalence $\text{finSuccEquiv'}$ evaluated at the last element of $\text{Fin}(n+1)$ maps the cast embedding $\text{castSucc}(i)$ to $i$ itself. In other words, $\text{finSuccEquiv'}\,(\text{last}\,n)\,(\text{castSucc}\,i) = i$.

finSuccEquiv'_last_apply theorem

{i : Fin (n + 1)} (h : i ≠ Fin.last n) : finSuccEquiv' (Fin.last n) i = Fin.castLT i (Fin.val_lt_last h)

Full source

theorem finSuccEquiv'_last_apply {i : Fin (n + 1)} (h : i ≠ Fin.last n) :
    finSuccEquiv' (Fin.last n) i = Fin.castLT i (Fin.val_lt_last h) := by
  rcases Fin.exists_castSucc_eq.2 h with ⟨i, rfl⟩
  rw [finSuccEquiv'_last_apply_castSucc]
  rfl

Equivalence at Last Element Maps Non-Last Elements via CastLT

Informal description

For any element $i \in \text{Fin}(n+1)$ such that $i \neq \text{last}(n)$, the equivalence $\text{finSuccEquiv'}$ evaluated at $\text{last}(n)$ maps $i$ to $\text{castLT}\,i\,(\text{val\_lt\_last}\,h)$, where $h$ is the proof that $i \neq \text{last}(n)$.

finSuccEquiv'_ne_last_apply theorem

 {i j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) :
  finSuccEquiv' i j = (i.castLT (Fin.val_lt_last hi)).predAbove j

Full source

theorem finSuccEquiv'_ne_last_apply {i j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) :
    finSuccEquiv' i j = (i.castLT (Fin.val_lt_last hi)).predAbove j := by
  rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
  rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
  simp

Mapping of Non-Last Elements via $\text{finSuccEquiv'}$ and $\text{predAbove}$

Informal description

For any two distinct elements $i, j \in \text{Fin}(n+1)$ such that $i$ is not the last element, the equivalence $\text{finSuccEquiv'}$ maps $j$ to the result of applying $\text{predAbove}$ to $j$ with respect to the cast of $i$ to $\text{Fin}(n)$. Specifically, we have: $$\text{finSuccEquiv'}\,i\,j = (\text{castLT}\,i\,(\text{val\_lt\_last}\,hi)).\text{predAbove}\,j$$ where: - $\text{castLT}\,i\,(\text{val\_lt\_last}\,hi)$ is the embedding of $i$ into $\text{Fin}(n)$ using the proof $hi$ that $i$ is not the last element - $\text{predAbove}$ is the operation that adjusts $j$ based on its position relative to $i$

finSuccAboveEquiv definition

(p : Fin (n + 1)) : Fin n ≃ { x : Fin (n + 1) // x ≠ p }

Full source

/-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`. -/
def finSuccAboveEquiv (p : Fin (n + 1)) : FinFin n ≃ { x : Fin (n + 1) // x ≠ p } :=
  .optionSubtype p ⟨(finSuccEquiv' p).symm, rfl⟩

Order isomorphism between $\text{Fin}\,n$ and $\{x \in \text{Fin}(n+1) \mid x \neq p\}$ via $\text{succAbove}$

Informal description

For a given element $p \in \text{Fin}(n+1)$, the equivalence $\text{finSuccAboveEquiv}\,p$ establishes an order isomorphism between $\text{Fin}\,n$ and the subtype $\{x \in \text{Fin}(n+1) \mid x \neq p\}$. The forward direction maps an element $i \in \text{Fin}\,n$ to $\langle p.\text{succAbove}\,i, p.\text{succAbove\_ne}\,i \rangle$, where: - $p.\text{succAbove}\,i$ is the element in $\text{Fin}(n+1)$ obtained by inserting $i$ above $p$. - $p.\text{succAbove\_ne}\,i$ is the proof that this element is not equal to $p$. The inverse direction reconstructs the original element in $\text{Fin}\,n$ from an element $x \in \{x \in \text{Fin}(n+1) \mid x \neq p\}$ by appropriately shifting the index.

finSuccAboveEquiv_apply theorem

(p : Fin (n + 1)) (i : Fin n) : finSuccAboveEquiv p i = ⟨p.succAbove i, p.succAbove_ne i⟩

Full source

theorem finSuccAboveEquiv_apply (p : Fin (n + 1)) (i : Fin n) :
    finSuccAboveEquiv p i = ⟨p.succAbove i, p.succAbove_ne i⟩ :=
  rfl

Application of the $\text{finSuccAboveEquiv}$ Equivalence

Informal description

For any natural number $n$, given an element $p \in \text{Fin}(n+1)$ and an element $i \in \text{Fin}(n)$, the equivalence $\text{finSuccAboveEquiv}$ maps $i$ to the pair $\langle p.\text{succAbove}\,i, p.\text{succAbove\_ne}\,i \rangle$, where: - $p.\text{succAbove}\,i$ is the embedding of $i$ into $\text{Fin}(n+1)$ with a hole at $p$, - $p.\text{succAbove\_ne}\,i$ is the proof that this embedding is not equal to $p$.

finSuccAboveEquiv_symm_apply_last theorem

 (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
  (finSuccAboveEquiv (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2)

Full source

theorem finSuccAboveEquiv_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
    (finSuccAboveEquiv (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2) := by
  rw [← Option.some_inj]
  simp [finSuccAboveEquiv]

Inverse of $\text{finSuccAboveEquiv}$ at Last Element via $\text{castLT}$

Informal description

For any element $x$ in $\text{Fin}(n+1)$ such that $x \neq \text{last}\,n$, the inverse of the equivalence $\text{finSuccAboveEquiv}$ applied to $x$ is equal to the cast of $x$ to $\text{Fin}\,n$ via $\text{castLT}$, where the proof that $x$ is less than $\text{last}\,n$ is given by $\text{val\_lt\_last}\,x.2$.

finSuccAboveEquiv_symm_apply_ne_last theorem

 {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x : Fin (n + 1) // x ≠ p }) :
  (finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x

Full source

theorem finSuccAboveEquiv_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
    (x : { x : Fin (n + 1) // x ≠ p }) :
    (finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x := by
  rw [← Option.some_inj]
  simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property

Inverse of $\text{finSuccAboveEquiv}$ for Non-Last Elements via $\text{predAbove}$

Informal description

For any element $p \in \text{Fin}(n+1)$ such that $p \neq \text{last}\,n$, and for any element $x \in \{x \in \text{Fin}(n+1) \mid x \neq p\}$, the inverse of the equivalence $\text{finSuccAboveEquiv}$ applied to $x$ is equal to $\text{predAbove}$ applied to $x$ with respect to the cast of $p$ to $\text{Fin}\,n$. Specifically: $$(\text{finSuccAboveEquiv}\,p)^{-1}(x) = (\text{castLT}\,p\,(\text{val\_lt\_last}\,h)).\text{predAbove}\,x$$ where: - $\text{castLT}\,p\,(\text{val\_lt\_last}\,h)$ is the embedding of $p$ into $\text{Fin}(n)$ using the proof $h$ that $p$ is not the last element, - $\text{predAbove}$ adjusts $x$ based on its position relative to $p$.

finSuccEquivLast definition

: Fin (n + 1) ≃ Option (Fin n)

Full source

/-- `Equiv` between `Fin (n + 1)` and `Option (Fin n)` sending `Fin.last n` to `none` -/
def finSuccEquivLast : FinFin (n + 1) ≃ Option (Fin n) :=
  finSuccEquiv' (Fin.last n)

Equivalence between $\text{Fin}(n+1)$ and $\text{Option}\,(\text{Fin}\,n)$ with last element mapped to none

Informal description

The equivalence $\text{finSuccEquivLast}$ between the finite type $\text{Fin}(n+1)$ and the option type $\text{Option}\,(\text{Fin}\,n)$ maps: - The last element $\text{Fin.last}\,n$ to $\text{none}$. - For any other element $i \in \text{Fin}(n+1)$, it maps $i$ to $\text{some}\,k$, where $k$ is the corresponding element in $\text{Fin}\,n$ obtained via the $\text{succAbove}$ operation. The inverse operation reconstructs the original element by: - Mapping $\text{none}$ back to $\text{Fin.last}\,n$. - Mapping $\text{some}\,k$ to the element obtained by applying $\text{succAbove}\,(\text{Fin.last}\,n)$ to $k$. This equivalence effectively removes the last element from $\text{Fin}(n+1)$ and shifts the remaining elements to $\text{Fin}\,n$, with the last element represented as $\text{none}$.

finSuccEquivLast_castSucc theorem

(i : Fin n) : finSuccEquivLast (Fin.castSucc i) = some i

Full source

@[simp]
theorem finSuccEquivLast_castSucc (i : Fin n) : finSuccEquivLast (Fin.castSucc i) = some i :=
  finSuccEquiv'_below i.2

$\text{finSuccEquivLast}$ Maps Cast Elements to Some in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

For any element $i \in \text{Fin}(n)$, the equivalence $\text{finSuccEquivLast}$ maps the cast of $i$ in $\text{Fin}(n+1)$ (denoted $\text{castSucc}\,i$) to $\text{some}\,i$ in $\text{Option}\,(\text{Fin}\,n)$. That is, $\text{finSuccEquivLast}(\text{castSucc}\,i) = \text{some}\,i$.

finSuccEquivLast_last theorem

: finSuccEquivLast (Fin.last n) = none

Full source

@[simp]
theorem finSuccEquivLast_last : finSuccEquivLast (Fin.last n) = none := by
  simp [finSuccEquivLast]

Last Element Maps to None in $\text{Fin}(n+1) \simeq \text{Option}\,(\text{Fin}\,n)$

Informal description

The equivalence `finSuccEquivLast` maps the last element of `Fin (n + 1)` to `none`, i.e., $\text{finSuccEquivLast}(\text{Fin.last}\,n) = \text{none}$.

finSuccEquivLast_symm_some theorem

(i : Fin n) : finSuccEquivLast.symm (some i) = Fin.castSucc i

Full source

@[simp]
theorem finSuccEquivLast_symm_some (i : Fin n) :
    finSuccEquivLast.symm (some i) = Fin.castSucc i :=
  finSuccEquiv'_symm_some_below i.2

Inverse of $\text{finSuccEquivLast}$ maps $\text{some}\,i$ to $\text{castSucc}\,i$

Informal description

For any natural number $n$ and any element $i \in \text{Fin}(n)$, the inverse of the equivalence $\text{finSuccEquivLast}$ maps $\text{some}\,i$ to the cast of $i$ in $\text{Fin}(n+1)$, i.e., $\text{finSuccEquivLast}^{-1}(\text{some}\,i) = \text{castSucc}\,i$.

finSuccEquivLast_symm_none theorem

: finSuccEquivLast.symm none = Fin.last n

Full source

@[simp] theorem finSuccEquivLast_symm_none : finSuccEquivLast.symm none = Fin.last n :=
  finSuccEquiv'_symm_none _

Inverse of $\text{finSuccEquivLast}$ maps $\text{none}$ to last element

Informal description

The inverse of the equivalence $\text{finSuccEquivLast}$ maps $\text{none}$ to the last element of $\text{Fin}(n+1)$, i.e., $\text{finSuccEquivLast}^{-1}(\text{none}) = \text{Fin.last}\,n$.

Equiv.embeddingFinSucc definition

(n : ℕ) (ι : Type*) : (Fin (n + 1) ↪ ι) ≃ (Σ (e : Fin n ↪ ι), { i // i ∉ Set.range e })

Full source

/-- 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`). -/
def Equiv.embeddingFinSucc (n : ℕ) (ι : Type*) :
    (Fin (n+1) ↪ ι) ≃ (Σ (e : Fin n ↪ ι), {i // i ∉ Set.range e}) :=
  ((finSuccEquiv n).embeddingCongr (Equiv.refl ι)).trans
    (Function.Embedding.optionEmbeddingEquiv (Fin n) ι)

Equivalence between embeddings of $\text{Fin}(n+1)$ and pairs of embeddings with an extra point

Informal description

The equivalence between embeddings of $\text{Fin}(n+1)$ into a type $\iota$ and pairs $(e, i)$, where $e$ is an embedding of $\text{Fin}(n)$ into $\iota$ and $i$ is an element of $\iota$ not in the range of $e$. Given an embedding $f : \text{Fin}(n+1) \hookrightarrow \iota$, the corresponding pair is obtained by restricting $f$ to $\text{Fin}(n)$ (via $\text{Fin.succ}$) and taking $f(0)$. Conversely, given an embedding $e : \text{Fin}(n) \hookrightarrow \iota$ and an element $i \in \iota$ not in the range of $e$, the corresponding embedding of $\text{Fin}(n+1)$ maps $0$ to $i$ and $k.\text{succ}$ to $e(k)$ for $k \in \text{Fin}(n)$.

Equiv.embeddingFinSucc_fst theorem

{n : ℕ} {ι : Type*} (e : Fin (n + 1) ↪ ι) : ((Equiv.embeddingFinSucc n ι e).1 : Fin n → ι) = e ∘ Fin.succ

Full source

@[simp] lemma Equiv.embeddingFinSucc_fst {n : ℕ} {ι : Type*} (e : FinFin (n+1) ↪ ι) :
    ((Equiv.embeddingFinSucc n ι e).1 : Fin n → ι) = e ∘ Fin.succ := rfl

First Component of Embedding Equivalence for $\text{Fin}(n+1)$ is Composition with Successor

Informal description

For any natural number $n$ and type $\iota$, given an embedding $e : \text{Fin}(n+1) \hookrightarrow \iota$, the first component of the equivalence $\text{embeddingFinSucc}$ applied to $e$ is equal to the composition of $e$ with the successor function on $\text{Fin}(n)$. That is, $(\text{embeddingFinSucc}(n, \iota)(e)).1 = e \circ \text{Fin.succ}$.

Equiv.embeddingFinSucc_snd theorem

{n : ℕ} {ι : Type*} (e : Fin (n + 1) ↪ ι) : ((Equiv.embeddingFinSucc n ι e).2 : ι) = e 0

Full source

@[simp] lemma Equiv.embeddingFinSucc_snd {n : ℕ} {ι : Type*} (e : FinFin (n+1) ↪ ι) :
    ((Equiv.embeddingFinSucc n ι e).2 : ι) = e 0 := rfl

Second Component of $\text{embeddingFinSucc}$ Equals $e(0)$

Informal description

For any natural number $n$ and type $\iota$, given an injective embedding $e : \text{Fin}(n+1) \hookrightarrow \iota$, the second component of the equivalence $\text{embeddingFinSucc}$ applied to $e$ is equal to $e(0)$. In other words, the element $i \in \iota$ not in the range of the restricted embedding $e \circ \text{Fin.succ}$ is exactly $e(0)$.

Equiv.coe_embeddingFinSucc_symm theorem

 {n : ℕ} {ι : Type*} (f : Σ (e : Fin n ↪ ι), { i // i ∉ Set.range e }) :
  ((Equiv.embeddingFinSucc n ι).symm f : Fin (n + 1) → ι) = Fin.cons f.2.1 f.1

Full source

@[simp] lemma Equiv.coe_embeddingFinSucc_symm {n : ℕ} {ι : Type*}
    (f : Σ (e : Fin n ↪ ι), {i // i ∉ Set.range e}) :
    ((Equiv.embeddingFinSucc n ι).symm f : Fin (n + 1) → ι) = Fin.cons f.2.1 f.1 := by
  ext i
  exact Fin.cases rfl (fun j ↦ rfl) i

Inverse of $\text{embeddingFinSucc}$ Constructs Dependent Tuple via $\text{Fin.cons}$

Informal description

For any natural number $n$ and type $\iota$, given a pair $(e, i)$ where $e : \text{Fin}(n) \hookrightarrow \iota$ is an embedding and $i \in \iota$ is not in the range of $e$, the function obtained by applying the inverse of the equivalence $\text{embeddingFinSucc}$ to $(e, i)$ is equal to the dependent tuple constructed by prepending $i$ to $e$ via $\text{Fin.cons}$. More precisely, for any $f = (e, i) \in \Sigma (e : \text{Fin}(n) \hookrightarrow \iota), \{ i \mid i \notin \text{range}(e) \}$, we have: \[ (\text{embeddingFinSucc}\, n\, \iota)^{-1}(f) = \text{Fin.cons}\, i\, e \]

finSumFinEquiv definition

: Fin m ⊕ Fin n ≃ Fin (m + n)

Full source

/-- Equivalence between `Fin m ⊕ Fin n` and `Fin (m + n)` -/
def finSumFinEquiv : FinFin m ⊕ Fin nFin m ⊕ Fin n ≃ Fin (m + n) where
  toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
  invFun i := @Fin.addCases m n (fun _ => FinFin m ⊕ Fin n) Sum.inl Sum.inr i
  left_inv x := by rcases x with y | y <;> dsimp <;> simp
  right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp

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

Informal description

The equivalence between the disjoint union of the canonical types with $m$ and $n$ elements, and the canonical type with $m + n$ elements. The forward map is defined by embedding the first summand via `Fin.castAdd n` and the second summand via `Fin.natAdd m`. The inverse map uses `Fin.addCases` to split an element of `Fin (m + n)` back into a sum based on whether it falls in the first $m$ or the remaining $n$ elements.

finSumFinEquiv_apply_left theorem

(i : Fin m) : (finSumFinEquiv (Sum.inl i) : Fin (m + n)) = Fin.castAdd n i

Full source

@[simp]
theorem finSumFinEquiv_apply_left (i : Fin m) :
    (finSumFinEquiv (Sum.inl i) : Fin (m + n)) = Fin.castAdd n i :=
  rfl

Left Injection under `finSumFinEquiv` Maps to `Fin.castAdd`

Informal description

For any element $i$ in $\text{Fin}\, m$, the equivalence $\text{finSumFinEquiv}$ maps the left injection of $i$ (i.e., $\text{Sum.inl}\, i$) to the element $\text{Fin.castAdd}\, n\, i$ in $\text{Fin}\, (m + n)$.

finSumFinEquiv_apply_right theorem

(i : Fin n) : (finSumFinEquiv (Sum.inr i) : Fin (m + n)) = Fin.natAdd m i

Full source

@[simp]
theorem finSumFinEquiv_apply_right (i : Fin n) :
    (finSumFinEquiv (Sum.inr i) : Fin (m + n)) = Fin.natAdd m i :=
  rfl

Right Injection under `finSumFinEquiv` Maps to `Fin.natAdd`

Informal description

For any element $i$ in $\text{Fin}\,n$, the equivalence $\text{finSumFinEquiv}$ maps the right injection of $i$ (i.e., $\text{Sum.inr}\,i$) to the element $\text{Fin.natAdd}\,m\,i$ in $\text{Fin}\,(m + n)$.

finSumFinEquiv_symm_apply_castAdd theorem

(x : Fin m) : finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x

Full source

@[simp]
theorem finSumFinEquiv_symm_apply_castAdd (x : Fin m) :
    finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x :=
  finSumFinEquiv.symm_apply_apply (Sum.inl x)

Inverse Equivalence Maps Cast Addition to Left Summand

Informal description

For any element $x$ in $\text{Fin}\,m$, the inverse of the equivalence $\text{finSumFinEquiv}$ maps the element $\text{Fin.castAdd}\,n\,x$ in $\text{Fin}\,(m + n)$ to the left summand $\text{Sum.inl}\,x$ in $\text{Fin}\,m \oplus \text{Fin}\,n$.

finSumFinEquiv_symm_apply_natAdd theorem

(x : Fin n) : finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x

Full source

@[simp]
theorem finSumFinEquiv_symm_apply_natAdd (x : Fin n) :
    finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x :=
  finSumFinEquiv.symm_apply_apply (Sum.inr x)

Inverse Equivalence Maps Natural Addition to Right Summand

Informal description

For any element $x$ of the finite type $\text{Fin}\,n$, the inverse of the equivalence $\text{finSumFinEquiv}$ maps the element $\text{Fin.natAdd}\,m\,x$ in $\text{Fin}\,(m + n)$ to the right summand $\text{Sum.inr}\,x$ in $\text{Fin}\,m \oplus \text{Fin}\,n$.

finSumFinEquiv_symm_last theorem

: finSumFinEquiv.symm (Fin.last n) = Sum.inr 0

Full source

@[simp]
theorem finSumFinEquiv_symm_last : finSumFinEquiv.symm (Fin.last n) = Sum.inr 0 :=
  finSumFinEquiv_symm_apply_natAdd 0

Inverse Equivalence Maps Last Element to Right Summand Zero

Informal description

The inverse of the equivalence between $\text{Fin}\,m \oplus \text{Fin}\,n$ and $\text{Fin}\,(m + n)$ maps the last element of $\text{Fin}\,(m + n)$ (i.e., $\text{Fin.last}\,n$) to the right summand $\text{Sum.inr}\,0$ in $\text{Fin}\,m \oplus \text{Fin}\,n$.

finAddFlip definition

: Fin (m + n) ≃ Fin (n + m)

Full source

/-- The equivalence between `Fin (m + n)` and `Fin (n + m)` which rotates by `n`. -/
def finAddFlip : FinFin (m + n) ≃ Fin (n + m) :=
  (finSumFinEquiv.symm.trans (Equiv.sumComm _ _)).trans finSumFinEquiv

Rotation equivalence between `Fin (m + n)` and `Fin (n + m)`

Informal description

The equivalence between the canonical types with $m + n$ and $n + m$ elements, which rotates by $n$ positions. This is constructed by composing the inverse of the equivalence between `Fin m ⊕ Fin n` and `Fin (m + n)` with the sum commutativity equivalence and then with the original equivalence.

finAddFlip_apply_castAdd theorem

(k : Fin m) (n : ℕ) : finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

Full source

@[simp]
theorem finAddFlip_apply_castAdd (k : Fin m) (n : ℕ) :
    finAddFlip (Fin.castAdd n k) = Fin.natAdd n k := by simp [finAddFlip]

Rotation Equivalence Maps Cast Addition to Natural Addition

Informal description

For any element $k$ in $\text{Fin}\,m$ and any natural number $n$, the rotation equivalence $\text{finAddFlip}$ maps the element $\text{Fin.castAdd}\,n\,k$ in $\text{Fin}\,(m + n)$ to $\text{Fin.natAdd}\,n\,k$ in $\text{Fin}\,(n + m)$.

finAddFlip_apply_natAdd theorem

(k : Fin n) (m : ℕ) : finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

Full source

@[simp]
theorem finAddFlip_apply_natAdd (k : Fin n) (m : ℕ) :
    finAddFlip (Fin.natAdd m k) = Fin.castAdd m k := by simp [finAddFlip]

Rotation Equivalence Maps Natural Addition to Cast Addition

Informal description

For any element $k$ in $\text{Fin}\,n$ and any natural number $m$, the rotation equivalence $\text{finAddFlip}$ maps the element $\text{Fin.natAdd}\,m\,k$ in $\text{Fin}\,(m + n)$ to $\text{Fin.castAdd}\,m\,k$ in $\text{Fin}\,(n + m)$.

finAddFlip_apply_mk_right theorem

{k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) : finAddFlip (⟨k, h₂⟩ : Fin (m + n)) = ⟨k - m, by omega⟩

Full source

@[simp]
theorem finAddFlip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
    finAddFlip (⟨k, h₂⟩ : Fin (m + n)) = ⟨k - m, by omega⟩ := by
  convert @finAddFlip_apply_natAdd n ⟨k - m, by omega⟩ m
  simp [Nat.add_sub_cancel' h₁]

Rotation Equivalence Maps Right Shifted Element to Subtracted Element

Informal description

For any natural number $k$ such that $m \leq k < m + n$, the rotation equivalence `finAddFlip` maps the element $\langle k, h_2 \rangle$ in $\text{Fin}(m + n)$ to $\langle k - m, \text{by omega} \rangle$ in $\text{Fin}(n + m)$, where $h_2$ is the proof that $k < m + n$.

finProdFinEquiv definition

: Fin m × Fin n ≃ Fin (m * n)

Full source

/-- Equivalence between `Fin m × Fin n` and `Fin (m * n)` -/
@[simps]
def finProdFinEquiv : FinFin m × Fin nFin m × Fin n ≃ Fin (m * n) where
  toFun x :=
    ⟨x.2 + n * x.1,
      calc
        x.2.1 + n * x.1.1 + 1 = x.1.1 * n + x.2.1 + 1 := by ac_rfl
        _ ≤ x.1.1 * n + n := Nat.add_le_add_left x.2.2 _
        _ = (x.1.1 + 1) * n := Eq.symm <| Nat.succ_mul _ _
        _ ≤ m * n := Nat.mul_le_mul_right _ x.1.2
        ⟩
  invFun x := (x.divNat, x.modNat)
  left_inv := fun ⟨x, y⟩ =>
    have H : 0 < n := Nat.pos_of_ne_zero fun H => Nat.not_lt_zero y.1 <| H ▸ y.2
    Prod.ext
      (Fin.eq_of_val_eq <|
        calc
          (y.1 + n * x.1) / n = y.1 / n + x.1 := Nat.add_mul_div_left _ _ H
          _ = 0 + x.1 := by rw [Nat.div_eq_of_lt y.2]
          _ = x.1 := Nat.zero_add x.1
          )
      (Fin.eq_of_val_eq <|
        calc
          (y.1 + n * x.1) % n = y.1 % n := Nat.add_mul_mod_self_left _ _ _
          _ = y.1 := Nat.mod_eq_of_lt y.2
          )
  right_inv _ := Fin.eq_of_val_eq <| Nat.mod_add_div _ _

Equivalence between product of finite types and finite product type

Informal description

The equivalence between the product type `Fin m × Fin n` and the finite type `Fin (m * n)`, where: - The forward map sends a pair `(x, y)` to the element `y + n * x` of `Fin (m * n)` - The inverse map sends an element `k` of `Fin (m * n)` to the pair `(k / n, k % n)`

Nat.divModEquiv definition

(n : ℕ) [NeZero n] : ℕ ≃ ℕ × Fin n

Full source

/-- 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. -/
@[simps]
def Nat.divModEquiv (n : ℕ) [NeZero n] : ℕℕ ≃ ℕ × Fin n where
  toFun a := (a / n, ↑a)
  invFun p := p.1 * n + ↑p.2
  -- TODO: is there a canonical order of `*` and `+` here?
  left_inv _ := Nat.div_add_mod' _ _
  right_inv p := by
    refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
    dsimp only
    rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]

Equivalence between natural numbers and pairs of quotient and remainder modulo $n$

Informal description

For any positive integer $n$, the equivalence $\mathrm{Nat.divModEquiv}\,n$ maps a natural number $a$ to the pair $(a / n, a \bmod n)$, where $a / n$ is the integer division of $a$ by $n$ and $a \bmod n$ is the remainder (represented as an element of $\mathrm{Fin}\,n$). The inverse function maps a pair $(q, r)$ to $q \cdot n + r$.

Int.divModEquiv definition

(n : ℕ) [NeZero n] : ℤ ≃ ℤ × Fin n

Full source

/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
See `Int.ediv_emod_unique` for a similar propositional statement. -/
@[simps]
def Int.divModEquiv (n : ℕ) [NeZero n] : ℤℤ ≃ ℤ × Fin n where
  -- TODO: could cast from int directly if we import `Data.ZMod.Defs`, though there are few lemmas
  -- about that coercion.
  toFun a := (a / n, ↑(a.natMod n))
  invFun p := p.1 * n + ↑p.2
  left_inv a := by
    simp_rw [Fin.coe_natCast_eq_mod, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_add_emod']
  right_inv := fun ⟨q, r, hrn⟩ => by
    simp only [Fin.val_mk, Prod.mk_inj, Fin.ext_iff]
    obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn
    rw [Int.add_comm, add_mul_ediv_right _ _ (natCast_eq_zero.not.2 (NeZero.ne n)),
      ediv_eq_zero_of_lt h1 h2, natMod, add_mul_emod_self_right, emod_eq_of_lt h1 h2, toNat_natCast]
    exact ⟨q.zero_add, Fin.val_cast_of_lt hrn⟩

Integer division-modulo equivalence

Informal description

For any positive integer $n$, the equivalence $\mathbb{Z} \simeq \mathbb{Z} \times \mathrm{Fin}\,n$ is defined by mapping an integer $a$ to the pair $(a / n, a \bmod n)$, where the modulo operation returns an element of $\mathrm{Fin}\,n$. The inverse operation maps a pair $(q, r)$ to $q \cdot n + r$.

Fin.castLEquiv definition

{n m : ℕ} (h : n ≤ m) : Fin n ≃ { i : Fin m // (i : ℕ) < n }

Full source

/-- 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`. -/
@[simps apply symm_apply]
def Fin.castLEquiv {n m : ℕ} (h : n ≤ m) : FinFin n ≃ { i : Fin m // (i : ℕ) < n } where
  toFun i := ⟨Fin.castLE h i, by simp⟩
  invFun i := ⟨i, i.prop⟩
  left_inv _ := by simp
  right_inv _ := by simp

Equivalence promoting `Fin n` to `Fin m` for $ n \leq m $

Informal description

Given natural numbers $ n $ and $ m $ with $ n \leq m $, the equivalence `Fin.castLEquiv h` promotes an element of the canonical type with $ n $ elements to an element of the canonical type with $ m $ elements, by embedding it as a subtype where the underlying value is preserved. Specifically, it maps $ i \in \text{Fin } n $ to $ \langle \text{Fin.castLE } h \, i, \text{proof} \rangle $, where the proof ensures that the underlying value remains less than $ n $. The inverse operation extracts the original element from the subtype.

subsingleton_fin_zero instance

: Subsingleton (Fin 0)

Full source

/-- `Fin 0` is a subsingleton. -/
instance subsingleton_fin_zero : Subsingleton (Fin 0) :=
  finZeroEquiv.subsingleton

$\text{Fin } 0$ is a Subsingleton

Informal description

The type $\text{Fin } 0$ of natural numbers less than 0 is a subsingleton (i.e., has at most one element).

subsingleton_fin_one instance

: Subsingleton (Fin 1)

Full source

/-- `Fin 1` is a subsingleton. -/
instance subsingleton_fin_one : Subsingleton (Fin 1) :=
  finOneEquiv.subsingleton

$\mathrm{Fin}\,1$ is a subsingleton

Informal description

The type $\mathrm{Fin}\,1$ (the finite type with one element) is a subsingleton, meaning any two elements of this type are equal.

Fin.appendEquiv definition

{α : Type*} (m n : ℕ) : (Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α)

Full source

/-- The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α` -/
@[simps]
def Fin.appendEquiv {α : Type*} (m n : ℕ) :
    (Fin m → α) × (Fin n → α)(Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α) where
  toFun fg := Fin.append fg.1 fg.2
  invFun f := ⟨fun i ↦ f (Fin.castAdd n i), fun i ↦ f (Fin.natAdd m i)⟩
  left_inv fg := by simp
  right_inv f := by simp [Fin.append_castAdd_natAdd]

Equivalence between concatenated tuples and functions on a larger finite type

Informal description

The natural equivalence between the product of function spaces $( \text{Fin}\, m \to \alpha ) \times ( \text{Fin}\, n \to \alpha )$ and the function space $\text{Fin}\, (m + n) \to \alpha$. Given a pair of functions $(f, g)$ where $f : \text{Fin}\, m \to \alpha$ and $g : \text{Fin}\, n \to \alpha$, the forward map constructs their concatenation $h : \text{Fin}\, (m + n) \to \alpha$ such that for $i < m$, $h\, i = f\, i$, and for $m \leq i < m + n$, $h\, i = g\, (i - m)$. The inverse map splits a function $h : \text{Fin}\, (m + n) \to \alpha$ into two functions $f : \text{Fin}\, m \to \alpha$ and $g : \text{Fin}\, n \to \alpha$ by restricting $h$ to the appropriate subdomains.