Documentation

Mathlib.Order.Fin.Basic

Fin n forms a bounded linear order #

This file contains the linear ordered instance on Fin n.

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions #

Instances #

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.

Miscellaneous lemmas #

theorem Fin.bot_eq_zero (n : ) [NeZero n] :
= 0
@[simp]
theorem Fin.rev_bot {n : } [NeZero n] :
@[simp]
theorem Fin.rev_top {n : } [NeZero n] :
@[simp]
theorem Fin.succ_top (n : ) [NeZero n] :
@[simp]
theorem Fin.val_top (n : ) [NeZero n] :
= n - 1
@[simp]
theorem Fin.zero_eq_top {n : } [NeZero n] :
0 = n = 1
@[simp]
theorem Fin.top_eq_zero {n : } [NeZero n] :
= 0 n = 1
@[simp]
theorem Fin.cast_top {m n : } [NeZero m] [NeZero n] (h : m = n) :
theorem Fin.strictMono_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : StrictMono f) :
StrictMono fun (a : α) => (f a).pred
theorem Fin.monotone_pred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a 0) (hf₂ : Monotone f) :
Monotone fun (a : α) => (f a).pred
theorem Fin.strictMono_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a last n) (hf₂ : StrictMono f) :
StrictMono fun (a : α) => (f a).castPred
theorem Fin.monotone_castPred_comp {n : } {α : Type u_1} [Preorder α] {f : αFin (n + 1)} (hf : ∀ (a : α), f a last n) (hf₂ : Monotone f) :
Monotone fun (a : α) => (f a).castPred
theorem Fin.strictMono_iff_lt_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
StrictMono f ∀ (i : Fin n), f i.castSucc < f i.succ

A function f on Fin (n + 1) is strictly monotone if and only if f i < f (i + 1) for all i.

theorem Fin.monotone_iff_le_succ {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
Monotone f ∀ (i : Fin n), f i.castSucc f i.succ

A function f on Fin (n + 1) is monotone if and only if f i ≤ f (i + 1) for all i.

theorem Fin.strictAnti_iff_succ_lt {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
StrictAnti f ∀ (i : Fin n), f i.succ < f i.castSucc

A function f on Fin (n + 1) is strictly antitone if and only if f (i + 1) < f i for all i.

theorem Fin.antitone_iff_succ_le {n : } {α : Type u_1} [Preorder α] {f : Fin (n + 1)α} :
Antitone f ∀ (i : Fin n), f i.succ f i.castSucc

A function f on Fin (n + 1) is antitone if and only if f (i + 1) ≤ f i for all i.

theorem Fin.orderHom_injective_iff {α : Type u_2} [PartialOrder α] {n : } (f : Fin (n + 1) →o α) :
Function.Injective f ∀ (i : Fin n), f i.castSucc f i.succ

Monotonicity #

theorem Fin.cast_strictMono {k l : } (h : k = l) :
theorem Fin.strictMono_castLE {m n : } (h : n m) :
theorem Fin.strictMono_addNat {n : } (m : ) :
StrictMono fun (x : Fin n) => x.addNat m
theorem Fin.succAbove_lt_succAbove_iff {n : } {p : Fin (n + 1)} {i j : Fin n} :
p.succAbove i < p.succAbove j i < j
theorem Fin.succAbove_le_succAbove_iff {n : } {p : Fin (n + 1)} {i j : Fin n} :
theorem Fin.predAbove_left_monotone {n : } (i : Fin (n + 1)) :
Monotone fun (p : Fin n) => p.predAbove i
def Fin.predAboveOrderHom {n : } (p : Fin n) :
Fin (n + 1) →o Fin n

Fin.predAbove p as an OrderHom.

Equations
@[simp]
theorem Fin.predAboveOrderHom_coe {n : } (p : Fin n) (i : Fin (n + 1)) :

Order isomorphisms #

def Fin.orderIsoSubtype {n : } :
Fin n ≃o { i : // i < n }

The equivalence Fin n ≃ {i // i < n} is an order isomorphism.

Equations
@[simp]
theorem Fin.orderIsoSubtype_symm_apply {n : } (a : { i : // i < n }) :
(RelIso.symm orderIsoSubtype) a = a,
@[simp]
theorem Fin.orderIsoSubtype_apply {n : } (a : Fin n) :
orderIsoSubtype a = a,
def Fin.castOrderIso {m n : } (eq : n = m) :

Fin.cast as an OrderIso.

castOrderIso eq i embeds i into an equal Fin type.

Equations
@[simp]
theorem Fin.castOrderIso_symm_apply {m n : } (eq : n = m) (i : Fin m) :
@[simp]
theorem Fin.castOrderIso_apply {m n : } (eq : n = m) (i : Fin n) :
(castOrderIso eq) i = Fin.cast eq i
@[simp]
theorem Fin.symm_castOrderIso {m n : } (h : n = m) :
@[simp]
theorem Fin.castOrderIso_refl {n : } (h : n = n := ) :
theorem Fin.castOrderIso_toEquiv {m n : } (h : n = m) :

While in many cases Fin.castOrderIso is better than Equiv.cast/cast, sometimes we want to apply a generic lemma about cast.

Fin.rev n as an order-reversing isomorphism.

Equations
@[simp]
theorem Fin.revOrderIso_apply {n : } (a✝ : (Fin n)ᵒᵈ) :

Order embeddings #

The inclusion map Fin n → ℕ is an order embedding.

Equations
@[simp]
theorem Fin.valOrderEmb_apply (n : ) (self : Fin n) :
(valOrderEmb n) self = self
instance Fin.Lt.isWellOrder (n : ) :
IsWellOrder (Fin n) fun (x1 x2 : Fin n) => x1 < x2

The ordering on Fin n is a well order.

@[simp]
def Fin.castLEOrderEmb {m n : } (h : n m) :

Fin.castLE as an OrderEmbedding.

castLEEmb h i embeds i into a larger Fin type.

Equations
@[simp]
theorem Fin.castLEOrderEmb_apply {m n : } (h : n m) (i : Fin n) :
@[simp]
theorem Fin.castLEOrderEmb_toEmbedding {m n : } (h : n m) :
(castLEOrderEmb h).toEmbedding = { toFun := castLE h, inj' := }
def Fin.castAddOrderEmb {n : } (m : ) :
Fin n ↪o Fin (n + m)

Fin.castAdd as an OrderEmbedding.

castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

Equations
@[simp]
theorem Fin.castAddOrderEmb_toEmbedding {n : } (m : ) :
(castAddOrderEmb m).toEmbedding = { toFun := castAdd m, inj' := }
@[simp]
theorem Fin.castAddOrderEmb_apply {n : } (m : ) (a✝ : Fin n) :
(castAddOrderEmb m) a✝ = castAdd m a✝
@[simp]
theorem Fin.castSuccOrderEmb_apply {n : } (a✝ : Fin n) :
@[simp]
def Fin.addNatOrderEmb {n : } (m : ) :
Fin n ↪o Fin (n + m)

Fin.addNat as an OrderEmbedding.

addNatOrderEmb m i adds m to i, generalizes Fin.succ.

Equations
@[simp]
theorem Fin.addNatOrderEmb_apply {n : } (m : ) (x✝ : Fin n) :
(addNatOrderEmb m) x✝ = x✝.addNat m
@[simp]
theorem Fin.addNatOrderEmb_toEmbedding {n : } (m : ) :
(addNatOrderEmb m).toEmbedding = { toFun := fun (x : Fin n) => x.addNat m, inj' := }
def Fin.natAddOrderEmb {m : } (n : ) :
Fin m ↪o Fin (n + m)

Fin.natAdd as an OrderEmbedding.

natAddOrderEmb n i adds n to i "on the left".

Equations
@[simp]
theorem Fin.natAddOrderEmb_apply {m : } (n : ) (i : Fin m) :
@[simp]
theorem Fin.natAddOrderEmb_toEmbedding {m : } (n : ) :
(natAddOrderEmb n).toEmbedding = { toFun := natAdd n, inj' := }
@[simp]
theorem Fin.succAboveOrderEmb_toEmbedding {n : } (p : Fin (n + 1)) :
p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := }
@[simp]
theorem Fin.succAboveOrderEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :

Uniqueness of order isomorphisms #

@[simp]
theorem Fin.coe_orderIso_apply {m n : } (e : Fin n ≃o Fin m) (i : Fin n) :
(e i) = i

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 : ℕ).

@[deprecated StrictMono.range_inj (since := "2024-09-17")]
theorem Fin.strictMono_unique {n : } {α : Type u_1} [Preorder α] {f g : Fin nα} (hf : StrictMono f) (hg : StrictMono g) (h : Set.range f = Set.range g) :
f = g

Two strictly monotone functions from Fin n are equal provided that their ranges are equal.

@[deprecated OrderEmbedding.range_inj (since := "2024-09-17")]
theorem Fin.orderEmbedding_eq {n : } {α : Type u_1} [Preorder α] {f g : Fin n ↪o α} (h : Set.range f = Set.range g) :
f = g

Two order embeddings of Fin n are equal provided that their ranges are equal.