Mathlib.Order.Fin.Basic

Fin.instLinearOrder instance

: LinearOrder (Fin n)

Full source

instance instLinearOrder : LinearOrder (Fin n) :=
  @LinearOrder.liftWithOrd (Fin n) _ _ ⟨fun x y => ⟨max x y, max_rec' (· < n) x.2 y.2⟩⟩
    ⟨fun x y => ⟨min x y, min_rec' (· < n) x.2 y.2⟩⟩ _ Fin.val Fin.val_injective (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Linear Order on Finite Types $\text{Fin } n$

Informal description

For any natural number $n$, the type $\text{Fin } n$ of natural numbers less than $n$ is equipped with a canonical linear order structure.

Fin.instBoundedOrder instance

[NeZero n] : BoundedOrder (Fin n)

Full source

instance instBoundedOrder [NeZero n] : BoundedOrder (Fin n) where
  top := rev 0
  le_top i := Nat.le_pred_of_lt i.is_lt
  bot := 0
  bot_le := Fin.zero_le'

Bounded Order Structure on Finite Types $\mathrm{Fin}\,n$

Informal description

For any nonzero natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a bounded order structure, where $0$ is the least element and $n-1$ is the greatest element.

Fin.instBiheytingAlgebra instance

[NeZero n] : BiheytingAlgebra (Fin n)

Full source

instance instBiheytingAlgebra [NeZero n] : BiheytingAlgebra (Fin n) :=
  LinearOrder.toBiheytingAlgebra

Bi-Heyting Algebra Structure on Finite Types $\mathrm{Fin}\,n$

Informal description

For any nonzero natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a bi-Heyting algebra structure.

Fin.coe_max theorem

(a b : Fin n) : ↑(max a b) = (max a b : ℕ)

Full source

@[simp, norm_cast]
theorem coe_max (a b : Fin n) : ↑(max a b) = (max a b : ℕ) := rfl

Maximum in $\text{Fin } n$ Commutes with Natural Number Embedding

Informal description

For any two elements $a$ and $b$ in $\text{Fin } n$, the canonical embedding of their maximum into the natural numbers equals the maximum of their embeddings, i.e., $\max(a, b) = \max(a, b)$ where the left-hand side is computed in $\text{Fin } n$ and the right-hand side is computed in $\mathbb{N}$.

Fin.coe_min theorem

(a b : Fin n) : ↑(min a b) = (min a b : ℕ)

Full source

@[simp, norm_cast]
theorem coe_min (a b : Fin n) : ↑(min a b) = (min a b : ℕ) := rfl

Minimum in $\text{Fin } n$ Commutes with Natural Number Embedding

Informal description

For any two elements $a$ and $b$ in $\text{Fin } n$, the canonical embedding of their minimum into the natural numbers equals the minimum of their embeddings, i.e., $\min(a, b) = \min(a, b)$ where the left-hand side is computed in $\text{Fin } n$ and the right-hand side is computed in $\mathbb{N}$.

Fin.instPartialOrder instance

: PartialOrder (Fin n)

Full source

instance instPartialOrder : PartialOrder (Fin n) := inferInstance

Partial Order on Finite Types $\text{Fin } n$

Informal description

For any natural number $n$, the type $\text{Fin } n$ of natural numbers less than $n$ is equipped with a canonical partial order structure.

Fin.instLattice instance

: Lattice (Fin n)

Full source

instance instLattice : Lattice (Fin n) := inferInstance

Lattice Structure on Finite Types $\text{Fin } n$

Informal description

For any natural number $n$, the type $\text{Fin } n$ of natural numbers less than $n$ is equipped with a canonical lattice structure.

Fin.instHeytingAlgebra instance

[NeZero n] : HeytingAlgebra (Fin n)

Full source

instance instHeytingAlgebra [NeZero n] : HeytingAlgebra (Fin n) := inferInstance

Heyting Algebra Structure on Finite Types $\mathrm{Fin}\,n$

Informal description

For any nonzero natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a Heyting algebra structure.

Fin.instCoheytingAlgebra instance

[NeZero n] : CoheytingAlgebra (Fin n)

Full source

instance instCoheytingAlgebra [NeZero n] : CoheytingAlgebra (Fin n) := inferInstance

Co-Heyting Algebra Structure on Finite Types $\mathrm{Fin}\,n$

Informal description

For any nonzero natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a co-Heyting algebra structure.

Fin.top_eq_last theorem

(n : ℕ) : ⊤ = Fin.last n

Full source

lemma top_eq_last (n : ℕ) : ⊤ = Fin.last n := rfl

Top Element Equals Last Element in $\mathrm{Fin}\,n$

Informal description

For any natural number $n$, the top element $\top$ in the finite type $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$) is equal to the last element $\mathrm{last}\,n$, which is the greatest element $n-1$ in $\mathrm{Fin}\,n$.

Fin.bot_eq_zero theorem

(n : ℕ) [NeZero n] : ⊥ = (0 : Fin n)

Full source

lemma bot_eq_zero (n : ℕ) [NeZero n] : ⊥ = (0 : Fin n) := rfl

Bottom Element in $\mathrm{Fin}\,n$ is Zero

Informal description

For any nonzero natural number $n$, the bottom element $\bot$ in the finite type $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$) is equal to $0$.

Fin.rev_bot theorem

[NeZero n] : rev (⊥ : Fin n) = ⊤

Full source

@[simp] theorem rev_bot [NeZero n] : rev (⊥ : Fin n) = ⊤ := rfl

Reverse of Bottom Element Equals Top in Finite Types

Informal description

For any nonzero natural number $n$, the reverse operation on the finite type $\mathrm{Fin}\,n$ maps the bottom element $\bot$ (which is $0$) to the top element $\top$ (which is the last element of $\mathrm{Fin}\,n$).

Fin.rev_top theorem

[NeZero n] : rev (⊤ : Fin n) = ⊥

Full source

@[simp] theorem rev_top [NeZero n] : rev (⊤ : Fin n) = ⊥ := rev_rev _

Reversal of Top Element in $\mathrm{Fin}\,n$ Equals Bottom

Informal description

For any nonzero natural number $n$, the reversal operation on the finite type $\mathrm{Fin}\,n$ maps the greatest element $\top$ to the least element $\bot$.

Fin.rev_zero_eq_top theorem

(n : ℕ) [NeZero n] : rev (0 : Fin n) = ⊤

Full source

theorem rev_zero_eq_top (n : ℕ) [NeZero n] : rev (0 : Fin n) = ⊤ := rfl

Reverse of Zero Equals Top in $\mathrm{Fin}\,n$

Informal description

For any nonzero natural number $n$, the reverse operation on the finite type $\mathrm{Fin}\,n$ maps the zero element $0$ to the top element $\top$.

Fin.rev_last_eq_bot theorem

(n : ℕ) : rev (last n) = ⊥

Full source

theorem rev_last_eq_bot (n : ℕ) : rev (last n) = ⊥ := by rw [rev_last, bot_eq_zero]

Reversal of Last Element in $\mathrm{Fin}\,n$ Equals Bottom

Informal description

For any natural number $n$, the reversal operation applied to the last element of $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$) yields the bottom element, i.e., $\mathrm{rev}(\mathrm{last}\,n) = \bot$.

Fin.succ_top theorem

(n : ℕ) [NeZero n] : (⊤ : Fin n).succ = ⊤

Full source

@[simp]
theorem succ_top (n : ℕ) [NeZero n] : (⊤ : Fin n).succ = ⊤ := by
  rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']

Successor of Top Element is Top in $\mathrm{Fin}\,n$

Informal description

For any positive natural number $n$ (i.e., $n \neq 0$), the successor of the greatest element in $\mathrm{Fin}\,n$ is itself, i.e., $\mathrm{succ}(\top) = \top$ in $\mathrm{Fin}\,n$.

Fin.val_top theorem

(n : ℕ) [NeZero n] : ((⊤ : Fin n) : ℕ) = n - 1

Full source

@[simp]
theorem val_top (n : ℕ) [NeZero n] : ((⊤ : Fin n) : ℕ) = n - 1 := rfl

Greatest Element in $\mathrm{Fin}\,n$ as Natural Number is $n-1$

Informal description

For any nonzero natural number $n$, the greatest element $\top$ in the finite type $\mathrm{Fin}\,n$ (natural numbers less than $n$) has a value equal to $n - 1$ when cast to a natural number, i.e., $(\top : \mathrm{Fin}\,n) = n - 1$.

Fin.zero_eq_top theorem

{n : ℕ} [NeZero n] : (0 : Fin n) = ⊤ ↔ n = 1

Full source

@[simp]
theorem zero_eq_top {n : ℕ} [NeZero n] : (0 : Fin n) = ⊤ ↔ n = 1 := by
  rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one, LE.le.le_iff_eq]
  exact pos_of_neZero n

Bottom Equals Top in $\mathrm{Fin}\,n$ iff $n=1$

Informal description

For any nonzero natural number $n$, the bottom element $0$ in $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$) equals the top element $\top$ if and only if $n = 1$.

Fin.top_eq_zero theorem

{n : ℕ} [NeZero n] : (⊤ : Fin n) = 0 ↔ n = 1

Full source

@[simp]
theorem top_eq_zero {n : ℕ} [NeZero n] : (⊤ : Fin n) = 0 ↔ n = 1 :=
  eq_comm.trans zero_eq_top

Top Equals Zero in $\mathrm{Fin}\,n$ iff $n=1$

Informal description

For any nonzero natural number $n$, the top element $\top$ in the finite type $\mathrm{Fin}\,n$ (natural numbers less than $n$) equals the zero element $0$ if and only if $n = 1$.

Fin.cast_top theorem

{m n : ℕ} [NeZero m] [NeZero n] (h : m = n) : (⊤ : Fin m).cast h = ⊤

Full source

@[simp]
theorem cast_top {m n : ℕ} [NeZero m] [NeZero n] (h : m = n) : (⊤ : Fin m).cast h = ⊤ := by
  simp [← val_inj, h]

Preservation of Top Element under Order Isomorphism of Finite Types

Informal description

For any two nonzero natural numbers $m$ and $n$ such that $m = n$, the top element $\top$ of $\mathrm{Fin}\,m$ is preserved under the order isomorphism $\mathrm{Fin}\,m \cong \mathrm{Fin}\,n$ induced by the equality $h : m = n$. That is, $\mathrm{cast}\,h\,\top = \top$.

Fin.strictMono_pred_comp theorem

(hf : ∀ a, f a ≠ 0) (hf₂ : StrictMono f) : StrictMono (fun a => pred (f a) (hf a))

Full source

lemma strictMono_pred_comp (hf : ∀ a, f a ≠ 0) (hf₂ : StrictMono f) :
    StrictMono (fun a => pred (f a) (hf a)) := fun _ _ h => pred_lt_pred_iff.2 (hf₂ h)

Strict Monotonicity of Predecessor Composition in Finite Types

Informal description

For any function $f$ from a type to $\text{Fin}(n)$ such that $f(a) \neq 0$ for all $a$ and $f$ is strictly monotone, the composition $\text{pred} \circ f$ is also strictly monotone. Here, $\text{pred}$ maps a non-zero element of $\text{Fin}(n)$ to its predecessor in $\text{Fin}(n-1)$.

Fin.monotone_pred_comp theorem

(hf : ∀ a, f a ≠ 0) (hf₂ : Monotone f) : Monotone (fun a => pred (f a) (hf a))

Full source

lemma monotone_pred_comp (hf : ∀ a, f a ≠ 0) (hf₂ : Monotone f) :
    Monotone (fun a => pred (f a) (hf a)) := fun _ _ h => pred_le_pred_iff.2 (hf₂ h)

Monotonicity Preservation under Composition with Predecessor in Finite Types

Informal description

For any function $f$ from a type to $\text{Fin}(n)$ such that $f(a) \neq 0$ for all $a$ and $f$ is monotone, the composition $\text{pred} \circ f$ is also monotone. Here, $\text{pred}$ maps a non-zero element of $\text{Fin}(n)$ to its predecessor in $\text{Fin}(n-1)$.

Fin.strictMono_castPred_comp theorem

(hf : ∀ a, f a ≠ last n) (hf₂ : StrictMono f) : StrictMono (fun a => castPred (f a) (hf a))

Full source

lemma strictMono_castPred_comp (hf : ∀ a, f a ≠ last n) (hf₂ : StrictMono f) :
    StrictMono (fun a => castPred (f a) (hf a)) := fun _ _ h => castPred_lt_castPred_iff.2 (hf₂ h)

Strict Monotonicity Preservation under Composition with Cast Predecessor in Finite Types

Informal description

For any function $f$ from a type to $\text{Fin}(n+1)$ such that $f(a) \neq \text{last}\,n$ for all $a$ and $f$ is strictly monotone, the composition $\text{castPred} \circ f$ is also strictly monotone. Here, $\text{castPred}$ maps an element of $\text{Fin}(n+1)$ that is not the last element to the corresponding element of $\text{Fin}(n)$.

Fin.monotone_castPred_comp theorem

(hf : ∀ a, f a ≠ last n) (hf₂ : Monotone f) : Monotone (fun a => castPred (f a) (hf a))

Full source

lemma monotone_castPred_comp (hf : ∀ a, f a ≠ last n) (hf₂ : Monotone f) :
    Monotone (fun a => castPred (f a) (hf a)) := fun _ _ h => castPred_le_castPred_iff.2 (hf₂ h)

Monotonicity of Composition with Cast Predecessor on Finite Types

Informal description

For any function $f \colon \alpha \to \mathrm{Fin}(n+1)$ such that $f(a) \neq \mathrm{last}\,n$ for all $a \in \alpha$ and $f$ is monotone, the composition $\mathrm{castPred} \circ f$ is also monotone. Here, $\mathrm{castPred}$ maps an element of $\mathrm{Fin}(n+1)$ that is not the last element to the corresponding element of $\mathrm{Fin}(n)$.

Fin.strictMono_iff_lt_succ theorem

: StrictMono f ↔ ∀ i : Fin n, f (castSucc i) < f i.succ

Full source

/-- A function `f` on `Fin (n + 1)` is strictly monotone if and only if `f i < f (i + 1)`
for all `i`. -/
lemma strictMono_iff_lt_succ : StrictMonoStrictMono f ↔ ∀ i : Fin n, f (castSucc i) < f i.succ :=
  liftFun_iff_succ (· < ·)

Characterization of Strictly Monotone Functions on $\mathrm{Fin}(n+1)$ via Successor Condition

Informal description

A function $f \colon \mathrm{Fin}(n+1) \to \alpha$ is strictly monotone if and only if for every $i \in \mathrm{Fin}(n)$, the value of $f$ at the embedding of $i$ into $\mathrm{Fin}(n+1)$ is strictly less than the value of $f$ at the successor of $i$, i.e., $f(\mathrm{castSucc}(i)) < f(i.\mathrm{succ})$.

Fin.monotone_iff_le_succ theorem

: Monotone f ↔ ∀ i : Fin n, f (castSucc i) ≤ f i.succ

Full source

/-- A function `f` on `Fin (n + 1)` is monotone if and only if `f i ≤ f (i + 1)` for all `i`. -/
lemma monotone_iff_le_succ : MonotoneMonotone f ↔ ∀ i : Fin n, f (castSucc i) ≤ f i.succ :=
  monotone_iff_forall_lt.trans <| liftFun_iff_succ (· ≤ ·)

Monotonicity Criterion for Functions on $\mathrm{Fin}(n+1)$ via Successor Condition

Informal description

A function $f \colon \mathrm{Fin}(n+1) \to \alpha$ is monotone if and only if for every $i \in \mathrm{Fin}(n)$, the value of $f$ at the embedding of $i$ into $\mathrm{Fin}(n+1)$ is less than or equal to the value of $f$ at the successor of $i$, i.e., $f(\mathrm{castSucc}(i)) \leq f(i.\mathrm{succ})$.

Fin.strictAnti_iff_succ_lt theorem

: StrictAnti f ↔ ∀ i : Fin n, f i.succ < f (castSucc i)

Full source

/-- A function `f` on `Fin (n + 1)` is strictly antitone if and only if `f (i + 1) < f i`
for all `i`. -/
lemma strictAnti_iff_succ_lt : StrictAntiStrictAnti f ↔ ∀ i : Fin n, f i.succ < f (castSucc i) :=
  liftFun_iff_succ (· > ·)

Characterization of Strictly Antitone Functions on $\mathrm{Fin}(n+1)$ via Successor Condition

Informal description

A function $f \colon \mathrm{Fin}(n+1) \to \alpha$ is strictly antitone if and only if for every $i \in \mathrm{Fin}(n)$, the value of $f$ at the successor of $i$ is strictly less than the value of $f$ at the embedding of $i$ into $\mathrm{Fin}(n+1)$, i.e., $f(i.\mathrm{succ}) < f(\mathrm{castSucc}(i))$.

Fin.antitone_iff_succ_le theorem

: Antitone f ↔ ∀ i : Fin n, f i.succ ≤ f (castSucc i)

Full source

/-- A function `f` on `Fin (n + 1)` is antitone if and only if `f (i + 1) ≤ f i` for all `i`. -/
lemma antitone_iff_succ_le : AntitoneAntitone f ↔ ∀ i : Fin n, f i.succ ≤ f (castSucc i) :=
  antitone_iff_forall_lt.trans <| liftFun_iff_succ (· ≥ ·)

Antitonicity Criterion for Functions on $\mathrm{Fin}(n+1)$ via Successor Condition

Informal description

A function $f \colon \mathrm{Fin}(n+1) \to \alpha$ is antitone if and only if for every $i \in \mathrm{Fin}(n)$, the value of $f$ at the successor of $i$ is less than or equal to the value of $f$ at the embedding of $i$ into $\mathrm{Fin}(n+1)$, i.e., $f(i.\mathrm{succ}) \leq f(\mathrm{castSucc}(i))$.

Fin.orderHom_injective_iff theorem

 {α : Type*} [PartialOrder α] {n : ℕ} (f : Fin (n + 1) →o α) :
  Function.Injective f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Full source

lemma orderHom_injective_iff {α : Type*} [PartialOrder α] {n : ℕ} (f : FinFin (n + 1) →o α) :
    Function.InjectiveFunction.Injective f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ := by
  constructor
  · intro hf i hi
    have := hf hi
    simp [Fin.ext_iff] at this
  · intro hf
    refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective
    exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

Injective Order Homomorphism Criterion for $\mathrm{Fin}(n+1)$ via Successor Inequality

Informal description

Let $\alpha$ be a partially ordered set and $n$ be a natural number. For any order homomorphism $f \colon \mathrm{Fin}(n+1) \to \alpha$, the following are equivalent: 1. $f$ is injective. 2. For every $i \in \mathrm{Fin}(n)$, the value of $f$ at the cast successor of $i$ is not equal to the value of $f$ at the successor of $i$, i.e., $f(i.\mathrm{castSucc}) \neq f(i.\mathrm{succ})$.

Fin.val_strictMono theorem

: StrictMono (val : Fin n → ℕ)

Full source

lemma val_strictMono : StrictMono (val : Fin n → ℕ) := fun _ _ ↦ id

Strict Monotonicity of the Natural Number Embedding for Finite Types

Informal description

The canonical embedding from $\text{Fin } n$ to $\mathbb{N}$, which maps each element of $\text{Fin } n$ to its underlying natural number, is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then their corresponding natural numbers satisfy $\text{val}(i) < \text{val}(j)$.

Fin.cast_strictMono theorem

{k l : ℕ} (h : k = l) : StrictMono (Fin.cast h)

Full source

lemma cast_strictMono {k l : ℕ} (h : k = l) : StrictMono (Fin.cast h) := fun {_ _} h ↦ h

Strict Monotonicity of the Finite Type Cast Function $\text{Fin.cast}_h$

Informal description

For any natural numbers $k$ and $l$ such that $k = l$, the function $\text{Fin.cast}_h : \text{Fin } k \to \text{Fin } l$ is strictly monotone. That is, for any $i, j \in \text{Fin } k$, if $i < j$ then $\text{Fin.cast}_h(i) < \text{Fin.cast}_h(j)$.

Fin.strictMono_succ theorem

: StrictMono (succ : Fin n → Fin (n + 1))

Full source

lemma strictMono_succ : StrictMono (succ : Fin n → Fin (n + 1)) := fun _ _ ↦ succ_lt_succ

Strict Monotonicity of the Successor Function on Finite Types

Informal description

The successor function $\text{succ} : \text{Fin } n \to \text{Fin } (n + 1)$ is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{succ}(i) < \text{succ}(j)$.

Fin.strictMono_castLE theorem

(h : n ≤ m) : StrictMono (castLE h : Fin n → Fin m)

Full source

lemma strictMono_castLE (h : n ≤ m) : StrictMono (castLE h : Fin n → Fin m) := fun _ _ ↦ id

Strict Monotonicity of the Finite Cast Embedding $\text{castLE}_h$

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, the embedding $\text{castLE}_h : \text{Fin } n \to \text{Fin } m$ (which casts elements of $\text{Fin } n$ to $\text{Fin } m$ via the inequality $h : n \leq m$) is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{castLE}_h(i) < \text{castLE}_h(j)$.

Fin.strictMono_castAdd theorem

(m) : StrictMono (castAdd m : Fin n → Fin (n + m))

Full source

lemma strictMono_castAdd (m) : StrictMono (castAdd m : Fin n → Fin (n + m)) := strictMono_castLE _

Strict Monotonicity of Right Addition on Finite Types

Informal description

For any natural number $m$, the embedding $\text{castAdd}_m : \text{Fin } n \to \text{Fin } (n + m)$ (which adds $m$ to the upper bound) is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{castAdd}_m(i) < \text{castAdd}_m(j)$.

Fin.strictMono_castSucc theorem

: StrictMono (castSucc : Fin n → Fin (n + 1))

Full source

lemma strictMono_castSucc : StrictMono (castSucc : Fin n → Fin (n + 1)) := strictMono_castAdd _

Strict Monotonicity of the Successor Cast on Finite Types

Informal description

The function $\text{castSucc} : \text{Fin } n \to \text{Fin } (n + 1)$, which embeds elements of $\text{Fin } n$ into $\text{Fin } (n + 1)$ by preserving their value, is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{castSucc}(i) < \text{castSucc}(j)$.

Fin.strictMono_natAdd theorem

(n) : StrictMono (natAdd n : Fin m → Fin (n + m))

Full source

lemma strictMono_natAdd (n) : StrictMono (natAdd n : Fin m → Fin (n + m)) :=
  fun i j h ↦ Nat.add_lt_add_left (show i.val < j.val from h) _

Strict Monotonicity of Left Addition on Finite Types

Informal description

For any natural numbers $n$ and $m$, the function $\text{natAdd}_n : \text{Fin } m \to \text{Fin } (n + m)$ defined by adding $n$ to the left is strictly monotone. That is, for any $i, j \in \text{Fin } m$, if $i < j$ then $\text{natAdd}_n(i) < \text{natAdd}_n(j)$.

Fin.strictMono_addNat theorem

(m) : StrictMono ((addNat · m) : Fin n → Fin (n + m))

Full source

lemma strictMono_addNat (m) : StrictMono ((addNat · m) : Fin n → Fin (n + m)) :=
  fun i j h ↦ Nat.add_lt_add_right (show i.val < j.val from h) _

Strict Monotonicity of Right Addition on Finite Types

Informal description

For any natural numbers $n$ and $m$, the function $f \colon \text{Fin } n \to \text{Fin } (n + m)$ defined by $f(i) = i + m$ is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $f(i) < f(j)$.

Fin.strictMono_succAbove theorem

(p : Fin (n + 1)) : StrictMono (succAbove p)

Full source

lemma strictMono_succAbove (p : Fin (n + 1)) : StrictMono (succAbove p) :=
  strictMono_castSucc.ite strictMono_succ
    (fun _ _ hij hj => (castSucc_lt_castSucc_iff.mpr hij).trans hj) fun i =>
    (castSucc_lt_succ i).le

Strict Monotonicity of the $\text{succAbove}_p$ Function on Finite Types

Informal description

For any natural number $n$ and any element $p \in \text{Fin } (n + 1)$, the function $\text{succAbove}_p : \text{Fin } n \to \text{Fin } (n + 1)$ is strictly monotone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{succAbove}_p(i) < \text{succAbove}_p(j)$.

Fin.succAbove_inj theorem

: succAbove p i = succAbove p j ↔ i = j

Full source

@[simp]
lemma succAbove_inj : succAbovesuccAbove p i = succAbove p j ↔ i = j :=
  (strictMono_succAbove p).injective.eq_iff

Injectivity of $\text{succAbove}_p$ on $\text{Fin } n$

Informal description

For any natural number $n$, element $p \in \text{Fin } (n + 1)$, and elements $i, j \in \text{Fin } n$, the equality $\text{succAbove}_p(i) = \text{succAbove}_p(j)$ holds if and only if $i = j$.

Fin.succAbove_le_succAbove_iff theorem

: succAbove p i ≤ succAbove p j ↔ i ≤ j

Full source

@[simp]
lemma succAbove_le_succAbove_iff : succAbovesuccAbove p i ≤ succAbove p j ↔ i ≤ j :=
  (strictMono_succAbove p).le_iff_le

Order Preservation of $\text{succAbove}_p$: $\text{succAbove}_p(i) \leq \text{succAbove}_p(j) \leftrightarrow i \leq j$

Informal description

For any natural number $n$, any element $p \in \text{Fin } (n + 1)$, and any elements $i, j \in \text{Fin } n$, the inequality $\text{succAbove}_p(i) \leq \text{succAbove}_p(j)$ holds if and only if $i \leq j$.

Fin.succAbove_lt_succAbove_iff theorem

: succAbove p i < succAbove p j ↔ i < j

Full source

@[simp]
lemma succAbove_lt_succAbove_iff : succAbovesuccAbove p i < succAbove p j ↔ i < j :=
  (strictMono_succAbove p).lt_iff_lt

Strict Order Preservation of $\text{succAbove}_p$: $\text{succAbove}_p(i) < \text{succAbove}_p(j) \leftrightarrow i < j$

Informal description

For any natural number $n$, any element $p \in \text{Fin } (n + 1)$, and any elements $i, j \in \text{Fin } n$, the strict inequality $\text{succAbove}_p(i) < \text{succAbove}_p(j)$ holds if and only if $i < j$ holds.

Fin.natAdd_inj theorem

(m) {i j : Fin n} : natAdd m i = natAdd m j ↔ i = j

Full source

@[simp]
theorem natAdd_inj (m) {i j : Fin n} : natAddnatAdd m i = natAdd m j ↔ i = j :=
  (strictMono_natAdd _).injective.eq_iff

Injectivity of Left Addition on Finite Types

Informal description

For any natural numbers $m$ and $n$, and for any elements $i, j \in \text{Fin } n$, the equality $\text{natAdd}_m(i) = \text{natAdd}_m(j)$ holds in $\text{Fin } (m + n)$ if and only if $i = j$ holds in $\text{Fin } n$.

Fin.natAdd_le_natAdd_iff theorem

(m) {i j : Fin n} : natAdd m i ≤ natAdd m j ↔ i ≤ j

Full source

@[simp]
theorem natAdd_le_natAdd_iff (m) {i j : Fin n} : natAddnatAdd m i ≤ natAdd m j ↔ i ≤ j :=
  (strictMono_natAdd _).le_iff_le

Left Addition Preserves Order in Finite Types

Informal description

For any natural numbers $m$ and $n$, and for any elements $i, j \in \text{Fin } n$, the inequality $\text{natAdd}_m(i) \leq \text{natAdd}_m(j)$ holds in $\text{Fin } (m + n)$ if and only if $i \leq j$ holds in $\text{Fin } n$.

Fin.natAdd_lt_natAdd_iff theorem

(m) {i j : Fin n} : natAdd m i < natAdd m j ↔ i < j

Full source

@[simp]
theorem natAdd_lt_natAdd_iff (m) {i j : Fin n} : natAddnatAdd m i < natAdd m j ↔ i < j :=
  (strictMono_natAdd _).lt_iff_lt

Left Addition Preserves Strict Order in Finite Types

Informal description

For any natural numbers $m$ and $n$, and for any elements $i, j \in \text{Fin } n$, the strict inequality $\text{natAdd}_m(i) < \text{natAdd}_m(j)$ holds in $\text{Fin } (m + n)$ if and only if $i < j$ holds in $\text{Fin } n$.

Fin.addNat_inj theorem

(m) {i j : Fin n} : i.addNat m = j.addNat m ↔ i = j

Full source

@[simp]
theorem addNat_inj (m) {i j : Fin n} : i.addNat m = j.addNat m ↔ i = j :=
  (strictMono_addNat _).injective.eq_iff

Injectivity of Right Addition in Finite Types

Informal description

For any natural numbers $n$ and $m$, and for any elements $i, j \in \text{Fin } n$, the equality $i + m = j + m$ holds in $\text{Fin } (n + m)$ if and only if $i = j$ holds in $\text{Fin } n$.

Fin.addNat_le_addNat_iff theorem

(m) {i j : Fin n} : i.addNat m ≤ j.addNat m ↔ i ≤ j

Full source

@[simp]
theorem addNat_le_addNat_iff (m) {i j : Fin n} : i.addNat m ≤ j.addNat m ↔ i ≤ j :=
  (strictMono_addNat _).le_iff_le

Order Preservation under Right Addition in Finite Types

Informal description

For any natural numbers $n$ and $m$, and for any elements $i, j \in \text{Fin } n$, the inequality $i + m \leq j + m$ holds in $\text{Fin } (n + m)$ if and only if $i \leq j$ holds in $\text{Fin } n$.

Fin.addNat_lt_addNat_iff theorem

(m) {i j : Fin n} : i.addNat m < j.addNat m ↔ i < j

Full source

@[simp]
theorem addNat_lt_addNat_iff (m) {i j : Fin n} : i.addNat m < j.addNat m ↔ i < j :=
  (strictMono_addNat _).lt_iff_lt

Strict Order Preservation under Right Addition in Finite Types

Informal description

For any natural numbers $n$ and $m$, and for any elements $i, j$ of $\text{Fin}\ n$, the strict inequality $i + m < j + m$ holds in $\text{Fin}\ (n + m)$ if and only if $i < j$ holds in $\text{Fin}\ n$.

Fin.castLE_le_castLE_iff theorem

{i j : Fin n} (h : n ≤ m) : i.castLE h ≤ j.castLE h ↔ i ≤ j

Full source

@[simp]
theorem castLE_le_castLE_iff {i j : Fin n} (h : n ≤ m) : i.castLE h ≤ j.castLE h ↔ i ≤ j := .rfl

Order Preservation under $\text{Fin.castLE}$ Embedding

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $i, j$ of $\text{Fin}\ n$, the inequality $i.\text{castLE}\ h \leq j.\text{castLE}\ h$ holds if and only if $i \leq j$ in $\text{Fin}\ n$. Here, $\text{castLE}\ h$ is the order-preserving embedding of $\text{Fin}\ n$ into $\text{Fin}\ m$ given by the hypothesis $h : n \leq m$.

Fin.castLE_lt_castLE_iff theorem

{i j : Fin n} (h : n ≤ m) : i.castLE h < j.castLE h ↔ i < j

Full source

@[simp]
theorem castLE_lt_castLE_iff {i j : Fin n} (h : n ≤ m) : i.castLE h < j.castLE h ↔ i < j := .rfl

Preservation of Strict Order under $\text{Fin}\ n$ Embedding via $\text{castLE}$

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any elements $i, j$ of $\text{Fin}\ n$, the inequality $i.\text{castLE}\ h < j.\text{castLE}\ h$ holds if and only if $i < j$ holds in $\text{Fin}\ n$.

Fin.predAbove_right_monotone theorem

(p : Fin n) : Monotone p.predAbove

Full source

lemma predAbove_right_monotone (p : Fin n) : Monotone p.predAbove := fun a b H => by
  dsimp [predAbove]
  split_ifs with ha hb hb
  all_goals simp only [le_iff_val_le_val, coe_pred]
  · exact pred_le_pred H
  · calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H
  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
  · exact H

Monotonicity of `predAbove` in the Second Argument

Informal description

For any natural number $n$ and any element $p \in \text{Fin}\ n$, the function $\text{predAbove}(p, \cdot)$ is monotone with respect to the natural order on $\text{Fin}\ (n + 1)$. That is, for any $i, j \in \text{Fin}\ (n + 1)$, if $i \leq j$, then $\text{predAbove}(p, i) \leq \text{predAbove}(p, j)$.

GCongr.Fin.predAbove_le_predAbove_right theorem

(p : Fin n) {i j : Fin (n + 1)} (h : i ≤ j) : p.predAbove i ≤ p.predAbove j

Full source

@[gcongr]
theorem _root_.GCongr.Fin.predAbove_le_predAbove_right (p : Fin n) {i j : Fin (n + 1)} (h : i ≤ j) :
    p.predAbove i ≤ p.predAbove j :=
  predAbove_right_monotone p h

Monotonicity of $\text{predAbove}$ in the Second Argument

Informal description

For any natural number $n$, any element $p \in \text{Fin}\ n$, and any elements $i, j \in \text{Fin}\ (n + 1)$ with $i \leq j$, the inequality $\text{predAbove}(p, i) \leq \text{predAbove}(p, j)$ holds.

Fin.predAbove_left_monotone theorem

(i : Fin (n + 1)) : Monotone fun p ↦ predAbove p i

Full source

lemma predAbove_left_monotone (i : Fin (n + 1)) : Monotone fun p ↦ predAbove p i := fun a b H ↦ by
  dsimp [predAbove]
  split_ifs with ha hb hb
  · rfl
  · exact pred_le _
  · have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
    exact absurd H this.not_le
  · rfl

Monotonicity of `predAbove` in the First Argument

Informal description

For any natural number $ n $ and any element $ i $ of $ \text{Fin} (n + 1) $, the function $ p \mapsto \text{predAbove}(p, i) $ is monotone with respect to the natural order on $ \text{Fin} n $. That is, for any $ p, q \in \text{Fin} n $, if $ p \leq q $, then $ \text{predAbove}(p, i) \leq \text{predAbove}(q, i) $.

GCongr.predAbove_le_predAbove_left theorem

{p q : Fin n} (h : p ≤ q) (i : Fin (n + 1)) : p.predAbove i ≤ q.predAbove i

Full source

@[gcongr]
lemma _root_.GCongr.predAbove_le_predAbove_left {p q : Fin n} (h : p ≤ q) (i : Fin (n + 1)) :
    p.predAbove i ≤ q.predAbove i :=
  predAbove_left_monotone i h

Monotonicity of $\text{predAbove}$ in First Argument: $\text{predAbove}(p, i) \leq \text{predAbove}(q, i)$ when $p \leq q$

Informal description

For any natural number $n$ and elements $p, q \in \text{Fin}\ n$ with $p \leq q$, and for any $i \in \text{Fin}\ (n + 1)$, we have $\text{predAbove}(p, i) \leq \text{predAbove}(q, i)$.

Fin.predAbove_le_predAbove theorem

{p q : Fin n} (hpq : p ≤ q) {i j : Fin (n + 1)} (hij : i ≤ j) : p.predAbove i ≤ q.predAbove j

Full source

@[gcongr]
lemma predAbove_le_predAbove {p q : Fin n} (hpq : p ≤ q) {i j : Fin (n + 1)} (hij : i ≤ j) :
    p.predAbove i ≤ q.predAbove j := by
  trans p.predAbove j <;> gcongr

Monotonicity of $\text{predAbove}$ in Both Arguments

Informal description

For any natural number $n$, elements $p, q \in \text{Fin}\ n$ with $p \leq q$, and elements $i, j \in \text{Fin}\ (n + 1)$ with $i \leq j$, we have $\text{predAbove}(p, i) \leq \text{predAbove}(q, j)$.

Fin.predAboveOrderHom definition

(p : Fin n) : Fin (n + 1) →o Fin n

Full source

/-- `Fin.predAbove p` as an `OrderHom`. -/
@[simps!] def predAboveOrderHom (p : Fin n) : FinFin (n + 1) →o Fin n :=
  ⟨p.predAbove, p.predAbove_right_monotone⟩

Order homomorphism version of `predAbove` for finite types

Informal description

For a given element $p$ in $\text{Fin}\ n$ (the type of natural numbers less than $n$), the function $\text{predAbove}(p, \cdot)$ is an order homomorphism from $\text{Fin}\ (n + 1)$ to $\text{Fin}\ n$. This means it is a monotone function that preserves the order relation: for any $i, j \in \text{Fin}\ (n + 1)$, if $i \leq j$, then $\text{predAbove}(p, i) \leq \text{predAbove}(p, j)$. More precisely, $\text{predAbove}(p, i)$ is defined as: - If $p < i$, then $\text{predAbove}(p, i) = i - 1$ (as an element of $\text{Fin}\ n$) - Otherwise, $\text{predAbove}(p, i) = i$ (cast down to $\text{Fin}\ n$)

Fin.orderIsoSubtype definition

: Fin n ≃o { i // i < n }

Full source

/-- The equivalence `Fin n ≃ {i // i < n}` is an order isomorphism. -/
@[simps! apply symm_apply]
def orderIsoSubtype : FinFin n ≃o {i // i < n} :=
  equivSubtype.toOrderIso (by simp [Monotone]) (by simp [Monotone])

Order isomorphism between $\text{Fin } n$ and natural numbers less than $n$

Informal description

The order isomorphism between the type $\text{Fin } n$ (the canonical type with $n$ elements) and the subtype $\{i \in \mathbb{N} \mid i < n\}$, where the bijection preserves the order relation in both directions. Specifically, for any $i, j \in \text{Fin } n$, we have $i \leq j$ if and only if their corresponding natural numbers in the subtype satisfy the same inequality.

Fin.castOrderIso definition

(eq : n = m) : Fin n ≃o Fin m

Full source

/-- `Fin.cast` as an `OrderIso`.

`castOrderIso eq i` embeds `i` into an equal `Fin` type. -/
@[simps]
def castOrderIso (eq : n = m) : FinFin n ≃o Fin m where
  toEquiv := ⟨Fin.cast eq, Fin.cast eq.symm, leftInverse_cast eq, rightInverse_cast eq⟩
  map_rel_iff' := cast_le_cast eq

Order isomorphism between `Fin n` and `Fin m` induced by equality `n = m`

Informal description

Given a proof `eq` that `n = m`, the function `Fin.castOrderIso eq` is an order isomorphism between the finite types `Fin n` and `Fin m`. This means it is a bijective function that preserves the order relation in both directions: for any `i, j : Fin n`, we have `i ≤ j` if and only if `Fin.cast eq i ≤ Fin.cast eq j`.

Fin.symm_castOrderIso theorem

(h : n = m) : (castOrderIso h).symm = castOrderIso h.symm

Full source

@[simp]
lemma symm_castOrderIso (h : n = m) : (castOrderIso h).symm = castOrderIso h.symm := by subst h; rfl

Inverse of Cast Order Isomorphism Equals Cast Order Isomorphism of Inverse

Informal description

For any natural numbers $n$ and $m$ with $n = m$, the inverse of the order isomorphism $\text{castOrderIso}\ h$ between $\text{Fin}\ n$ and $\text{Fin}\ m$ is equal to the order isomorphism $\text{castOrderIso}\ h^{-1}$ between $\text{Fin}\ m$ and $\text{Fin}\ n$.

Fin.castOrderIso_toEquiv theorem

(h : n = m) : (castOrderIso h).toEquiv = Equiv.cast (h ▸ rfl)

Full source

/-- While in many cases `Fin.castOrderIso` is better than `Equiv.cast`/`cast`, sometimes we want to
apply a generic lemma about `cast`. -/
lemma castOrderIso_toEquiv (h : n = m) : (castOrderIso h).toEquiv = Equiv.cast (h ▸ rfl) := by
  subst h; rfl

Equivalence of `Fin.castOrderIso` equals `Equiv.cast`

Informal description

Given a proof $h$ that $n = m$, the underlying equivalence of the order isomorphism `Fin.castOrderIso h` is equal to the equivalence obtained by casting along $h$ (i.e., `Equiv.cast (h ▸ rfl)`).

Fin.revOrderIso definition

: (Fin n)ᵒᵈ ≃o Fin n

Full source

/-- `Fin.rev n` as an order-reversing isomorphism. -/
@[simps! apply toEquiv]
def revOrderIso : (Fin n)ᵒᵈ(Fin n)ᵒᵈ ≃o Fin n := ⟨OrderDual.ofDual.trans revPerm, rev_le_rev⟩

Order-reversing isomorphism on finite types

Informal description

The order isomorphism $\text{revOrderIso}$ maps the order-dual of $\text{Fin } n$ to $\text{Fin } n$ via the antitone involution $i \mapsto n - (i + 1)$, where $i$ is an element of $\text{Fin } n$. This isomorphism reverses the order relation, meaning that for any $i, j \in \text{Fin } n$, we have $i \leq j$ in the dual order if and only if $\text{rev}(j) \leq \text{rev}(i)$ in the standard order.

Fin.revOrderIso_symm_apply theorem

(i : Fin n) : revOrderIso.symm i = OrderDual.toDual (rev i)

Full source

@[simp]
lemma revOrderIso_symm_apply (i : Fin n) : revOrderIso.symm i = OrderDual.toDual (rev i) := rfl

Inverse of Order-Reversing Isomorphism on Finite Types Applies to Reversal

Informal description

For any element $i$ in $\text{Fin } n$, the application of the inverse of the order-reversing isomorphism $\text{revOrderIso}$ to $i$ is equal to the dual of the reversal of $i$, i.e., $\text{revOrderIso}^{-1}(i) = \text{OrderDual.toDual}(\text{rev}(i))$.

Fin.rev_strictAnti theorem

: StrictAnti (@rev n)

Full source

lemma rev_strictAnti : StrictAnti (@rev n) := fun _ _ ↦ rev_lt_rev.mpr

Strict Antitonicity of the Reversal Function on Finite Types

Informal description

The function $\text{rev} : \text{Fin } n \to \text{Fin } n$, defined by $\text{rev}(i) = n - (i + 1)$, is strictly antitone. That is, for any $i, j \in \text{Fin } n$, if $i < j$ then $\text{rev}(j) < \text{rev}(i)$.

Fin.rev_anti theorem

: Antitone (@rev n)

Full source

lemma rev_anti : Antitone (@rev n) := rev_strictAnti.antitone

Antitonicity of the Finite Reversal Function

Informal description

The reversal function $\text{rev} : \text{Fin } n \to \text{Fin } n$, defined by $\text{rev}(i) = n - (i + 1)$, is antitone. That is, for any $i, j \in \text{Fin } n$, if $i \leq j$ then $\text{rev}(j) \leq \text{rev}(i)$.

Fin.valOrderEmb definition

(n) : Fin n ↪o ℕ

Full source

/-- The inclusion map `Fin n → ℕ` is an order embedding. -/
@[simps! apply]
def valOrderEmb (n) : FinFin n ↪o ℕ := ⟨valEmbedding, Iff.rfl⟩

Order embedding of finite types into natural numbers

Informal description

The inclusion map from the finite type $\mathrm{Fin}\,n$ (natural numbers less than $n$) to the natural numbers $\mathbb{N}$ is an order embedding, meaning it preserves the order relation: for any $x, y \in \mathrm{Fin}\,n$, $x \leq y$ if and only if their underlying natural number values satisfy $x \leq y$.

Fin.Lt.isWellOrder instance

(n) : IsWellOrder (Fin n) (· < ·)

Full source

/-- The ordering on `Fin n` is a well order. -/
instance Lt.isWellOrder (n) : IsWellOrder (Fin n) (· < ·) := (valOrderEmb n).isWellOrder

Well-Ordering of Finite Types $\mathrm{Fin}\,n$

Informal description

For any natural number $n$, the strict order $<$ on the finite type $\mathrm{Fin}\,n$ (natural numbers less than $n$) is a well-order. That is, it is a strict total order where every non-empty subset has a minimal element with respect to $<$.

Fin.succOrderEmb definition

(n : ℕ) : Fin n ↪o Fin (n + 1)

Full source

/-- `Fin.succ` as an `OrderEmbedding` -/
def succOrderEmb (n : ℕ) : FinFin n ↪o Fin (n + 1) := .ofStrictMono succ strictMono_succ

Order embedding of the successor function on finite types

Informal description

The successor function $\text{succ} : \text{Fin } n \to \text{Fin } (n + 1)$, which maps each element $i$ of the finite type $\text{Fin } n$ to $i + 1$, is an order embedding. This means it is injective and preserves the order relation: for any $i, j \in \text{Fin } n$, $i \leq j$ if and only if $\text{succ}(i) \leq \text{succ}(j)$ in $\text{Fin } (n + 1)$.

Fin.coe_succOrderEmb theorem

: ⇑(succOrderEmb n) = Fin.succ

Full source

@[simp, norm_cast] lemma coe_succOrderEmb : ⇑(succOrderEmb n) = Fin.succ := rfl

Underlying Function of Successor Order Embedding Equals `Fin.succ`

Informal description

The underlying function of the order embedding `succOrderEmb` from `Fin n` to `Fin (n + 1)` is equal to the successor function `Fin.succ`.

Fin.succOrderEmb_toEmbedding theorem

: (succOrderEmb n).toEmbedding = succEmb n

Full source

@[simp] lemma succOrderEmb_toEmbedding : (succOrderEmb n).toEmbedding = succEmb n := rfl

Underlying Embedding of Successor Order Embedding Equals Successor Embedding

Informal description

The underlying embedding of the successor order embedding on $\text{Fin } n$ is equal to the successor embedding on $\text{Fin } n$.

Fin.castLEOrderEmb definition

(h : n ≤ m) : Fin n ↪o Fin m

Full source

/-- `Fin.castLE` as an `OrderEmbedding`.

`castLEEmb h i` embeds `i` into a larger `Fin` type. -/
@[simps! apply toEmbedding]
def castLEOrderEmb (h : n ≤ m) : FinFin n ↪o Fin m := .ofStrictMono (castLE h) (strictMono_castLE h)

Order embedding of finite types via inequality $n \leq m$

Informal description

For natural numbers $n$ and $m$ with $n \leq m$, the order embedding $\text{Fin.castLEOrderEmb}_h : \text{Fin } n \hookrightarrow \text{Fin } m$ is defined by casting elements of $\text{Fin } n$ to $\text{Fin } m$ via the inequality $h : n \leq m$. This embedding is strictly monotone, meaning it preserves the order relation: for any $i, j \in \text{Fin } n$, $i < j$ implies $\text{castLEOrderEmb}_h(i) < \text{castLEOrderEmb}_h(j)$.

Fin.castAddOrderEmb definition

(m) : Fin n ↪o Fin (n + m)

Full source

/-- `Fin.castAdd` as an `OrderEmbedding`.

`castAddEmb m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAddEmb` and `Fin.addNatEmb`. -/
@[simps! apply toEmbedding]
def castAddOrderEmb (m) : FinFin n ↪o Fin (n + m) := .ofStrictMono (castAdd m) (strictMono_castAdd m)

Order embedding of right addition on finite types

Informal description

The order embedding `Fin.castAddOrderEmb m` maps each element `i` of the finite type `Fin n` (natural numbers less than `n`) to the corresponding element in `Fin (n + m)` (natural numbers less than `n + m`), preserving the order. This embedding is strictly monotone, meaning that if `i < j` in `Fin n`, then their images under the embedding satisfy the same inequality in `Fin (n + m)`.

Fin.castSuccOrderEmb definition

: Fin n ↪o Fin (n + 1)

Full source

/-- `Fin.castSucc` as an `OrderEmbedding`.

`castSuccOrderEmb i` embeds `i : Fin n` in `Fin (n+1)`. -/
@[simps! apply toEmbedding]
def castSuccOrderEmb : FinFin n ↪o Fin (n + 1) := .ofStrictMono castSucc strictMono_castSucc

Order embedding of $\text{Fin } n$ into $\text{Fin } (n + 1)$ via value-preserving inclusion

Informal description

The order embedding that maps each element $i$ of the finite type $\text{Fin } n$ (natural numbers less than $n$) to the corresponding element in $\text{Fin } (n + 1)$ by preserving its value. This embedding is strictly monotone, meaning that if $i < j$ in $\text{Fin } n$, then their images under this embedding satisfy the same inequality in $\text{Fin } (n + 1)$.

Fin.addNatOrderEmb definition

(m) : Fin n ↪o Fin (n + m)

Full source

/-- `Fin.addNat` as an `OrderEmbedding`.

`addNatOrderEmb m i` adds `m` to `i`, generalizes `Fin.succ`. -/
@[simps! apply toEmbedding]
def addNatOrderEmb (m) : FinFin n ↪o Fin (n + m) := .ofStrictMono (addNat · m) (strictMono_addNat m)

Order embedding of right addition on finite types

Informal description

For any natural numbers $n$ and $m$, the function that adds $m$ to each element of $\text{Fin } n$ (the type of natural numbers less than $n$) is an order embedding from $\text{Fin } n$ to $\text{Fin } (n + m)$. This means the function is injective and preserves the order relation: for any $i, j \in \text{Fin } n$, $i \leq j$ if and only if $i + m \leq j + m$ in $\text{Fin } (n + m)$.

Fin.natAddOrderEmb definition

(n) : Fin m ↪o Fin (n + m)

Full source

/-- `Fin.natAdd` as an `OrderEmbedding`.

`natAddOrderEmb n i` adds `n` to `i` "on the left". -/
@[simps! apply toEmbedding]
def natAddOrderEmb (n) : FinFin m ↪o Fin (n + m) := .ofStrictMono (natAdd n) (strictMono_natAdd n)

Order embedding of left addition on finite types

Informal description

For natural numbers $n$ and $m$, the function $\text{natAdd}_n : \text{Fin } m \to \text{Fin } (n + m)$ that adds $n$ to the left (i.e., $\text{natAdd}_n(i) = n + i$) is an order embedding. This means it is injective and preserves the order relation: for any $i, j \in \text{Fin } m$, $i \leq j$ if and only if $\text{natAdd}_n(i) \leq \text{natAdd}_n(j)$.

Fin.succAboveOrderEmb definition

(p : Fin (n + 1)) : Fin n ↪o Fin (n + 1)

Full source

/-- `Fin.succAbove p` as an `OrderEmbedding`. -/
@[simps! apply toEmbedding]
def succAboveOrderEmb (p : Fin (n + 1)) : FinFin n ↪o Fin (n + 1) :=
  OrderEmbedding.ofStrictMono (succAbove p) (strictMono_succAbove p)

Order embedding of $\text{Fin } n$ into $\text{Fin } (n + 1)$ with a hole at $ p $

Informal description

For any natural number $ n $ and any element $ p \in \text{Fin } (n + 1) $, the function $\text{succAbove}_p : \text{Fin } n \hookrightarrow \text{Fin } (n + 1)$ is an order embedding. This means it is an injective function that preserves the order relation: for any $ i, j \in \text{Fin } n $, $ i \leq j $ if and only if $\text{succAbove}_p(i) \leq \text{succAbove}_p(j) $.

Fin.coe_orderIso_apply theorem

(e : Fin n ≃o Fin m) (i : Fin n) : (e i : ℕ) = i

Full source

/-- If `e` is an `orderIso` between `Fin n` and `Fin m`, then `n = m` and `e` is the identity
map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i : ℕ)`. -/
@[simp] lemma coe_orderIso_apply (e : FinFin n ≃o Fin m) (i : Fin n) : (e i : ℕ) = i := by
  rcases i with ⟨i, hi⟩
  dsimp only
  induction' i using Nat.strong_induction_on with i h
  refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)
  · have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
    specialize h _ this (e.symm _).is_lt
    simp only [Fin.eta, OrderIso.apply_symm_apply] at h
    rwa [h]
  · rwa [← h j hj (hj.trans hi), ← lt_iff_val_lt_val, e.lt_iff_lt]

Order Isomorphism on Finite Types Preserves Natural Number Representation

Informal description

Let $e \colon \text{Fin } n \simeq_o \text{Fin } m$ be an order isomorphism between the finite types $\text{Fin } n$ and $\text{Fin } m$. Then for every $i \in \text{Fin } n$, the natural number corresponding to $e(i)$ is equal to $i$ itself, i.e., $e(i) = i$ (as natural numbers).

Main definitions