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

• Fin.orderIsoSubtype : coercion to {i // i < n} as an OrderIso;
• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.valOrderEmb : coercion to natural numbers as an OrderEmbedding;
• Fin.succOrderEmb : Fin.succ as an OrderEmbedding;
• Fin.castLEOrderEmb h : Fin.castLE as an OrderEmbedding, embed Fin n into Fin m when h : n ≤ m;
• Fin.castOrderIso : Fin.cast as an OrderIso, order isomorphism between Fin n and Fin m provided that n = m, see also Equiv.finCongr;
• Fin.castAddOrderEmb m : Fin.castAdd as an OrderEmbedding, embed Fin n into Fin (n+m);
• Fin.castSuccOrderEmb : Fin.castSucc as an OrderEmbedding, embed Fin n into Fin (n+1);
• Fin.addNatOrderEmb m i : Fin.addNat as an OrderEmbedding, add m on i on the right, generalizes Fin.succ;
• Fin.natAddOrderEmb n i : Fin.natAdd as an OrderEmbedding, adds n on i on the left;
• Fin.revOrderIso: Fin.rev as an OrderIso, the antitone involution given by i ↦ n-(i+1)

Instances

instance Fin.instLinearOrder {n : ℕ} : LinearOrder (Fin n)

Equations

• Fin.instLinearOrder = LinearOrder.liftWithOrd Fin.val ⋯ ⋯ ⋯ ⋯

instance Fin.instBoundedOrder {n : ℕ} [NeZero n] : BoundedOrder (Fin n)

Equations

• Fin.instBoundedOrder = BoundedOrder.mk

Extra instances to short-circuit type class resolution

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

instance Fin.instPartialOrder {n : ℕ} : PartialOrder (Fin n)

Equations

• Fin.instPartialOrder = inferInstance

instance Fin.instLattice {n : ℕ} : Lattice (Fin n)

Equations

• Fin.instLattice = inferInstance

Miscellaneous lemmas

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

theorem Fin.bot_eq_zero (n : ℕ) : ⊥ = 0

@[simp]

theorem Fin.rev_bot {n : ℕ} [NeZero n] : ⊥.rev = ⊤

@[simp]

theorem Fin.rev_top {n : ℕ} [NeZero n] : ⊤.rev = ⊥

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

theorem Fin.rev_last_eq_bot (n : ℕ) : (Fin.last n).rev = ⊥

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 ≠ Fin.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 ≠ Fin.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.

Monotonicity

theorem Fin.val_strictMono {n : ℕ} : StrictMono Fin.val

theorem Fin.strictMono_succ {n : ℕ} : StrictMono Fin.succ

theorem Fin.strictMono_castLE {m : ℕ} {n : ℕ} (h : n ≤ m) : StrictMono (Fin.castLE h)

theorem Fin.strictMono_castAdd {n : ℕ} (m : ℕ) : StrictMono (Fin.castAdd m)

theorem Fin.strictMono_castSucc {n : ℕ} : StrictMono Fin.castSucc

theorem Fin.strictMono_natAdd {m : ℕ} (n : ℕ) : StrictMono (Fin.natAdd n)

theorem Fin.strictMono_addNat {n : ℕ} (m : ℕ) : StrictMono fun (x : Fin n) => x.addNat m

theorem Fin.strictMono_succAbove {n : ℕ} (p : Fin (n + 1)) : StrictMono p.succAbove

theorem Fin.succAbove_lt_succAbove_iff {n : ℕ} {p : Fin (n + 1)} {i : Fin n} {j : Fin n} : p.succAbove i < p.succAbove j ↔ i < j

theorem Fin.succAbove_le_succAbove_iff {n : ℕ} {p : Fin (n + 1)} {i : Fin n} {j : Fin n} : p.succAbove i ≤ p.succAbove j ↔ i ≤ j

theorem Fin.predAbove_right_monotone {n : ℕ} (p : Fin n) : Monotone p.predAbove

theorem Fin.predAbove_left_monotone {n : ℕ} (i : Fin (n + 1)) : Monotone fun (p : Fin n) => p.predAbove i

@[simp]

theorem Fin.predAboveOrderHom_coe {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : p.predAboveOrderHom i = p.predAbove i

def Fin.predAboveOrderHom {n : ℕ} (p : Fin n) : Fin (n + 1) →o Fin n

Fin.predAbove p as an OrderHom.

Equations

• p.predAboveOrderHom = { toFun := p.predAbove, monotone' := ⋯ }

Order isomorphisms

@[simp]

theorem Fin.orderIsoSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) : (RelIso.symm Fin.orderIsoSubtype) a = ⟨↑a, ⋯⟩

@[simp]

theorem Fin.orderIsoSubtype_apply {n : ℕ} (a : Fin n) : Fin.orderIsoSubtype a = ⟨↑a, ⋯⟩

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

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

Equations

• Fin.orderIsoSubtype = Fin.equivSubtype.toOrderIso ⋯ ⋯

@[simp]

theorem Fin.castOrderIso_symm_apply {m : ℕ} {n : ℕ} (eq : n = m) (i : Fin m) : (RelIso.symm (Fin.castOrderIso eq)) i = Fin.cast ⋯ i

@[simp]

theorem Fin.castOrderIso_apply {m : ℕ} {n : ℕ} (eq : n = m) (i : Fin n) : (Fin.castOrderIso eq) i = Fin.cast eq i

def Fin.castOrderIso {m : ℕ} {n : ℕ} (eq : n = m) : Fin n ≃o Fin m

Fin.cast as an OrderIso.

castOrderIso eq i embeds i into an equal Fin type.

Equations

• Fin.castOrderIso eq = { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[deprecated Fin.castOrderIso]

def Fin.castIso {m : ℕ} {n : ℕ} (eq : n = m) : Fin n ≃o Fin m

Alias of Fin.castOrderIso.

---

Fin.cast as an OrderIso.

castOrderIso eq i embeds i into an equal Fin type.

Equations

• @Fin.castIso = @Fin.castOrderIso

@[simp]

theorem Fin.symm_castOrderIso {m : ℕ} {n : ℕ} (h : n = m) : (Fin.castOrderIso h).symm = Fin.castOrderIso ⋯

@[deprecated Fin.symm_castOrderIso]

theorem Fin.symm_castIso {m : ℕ} {n : ℕ} (h : n = m) : (Fin.castOrderIso h).symm = Fin.castOrderIso ⋯

Alias of Fin.symm_castOrderIso.

@[simp]

theorem Fin.castOrderIso_refl {n : ℕ} (h : optParam (n = n) ⋯) : Fin.castOrderIso h = OrderIso.refl (Fin n)

@[deprecated Fin.castOrderIso_refl]

theorem Fin.castIso_refl {n : ℕ} (h : optParam (n = n) ⋯) : Fin.castOrderIso h = OrderIso.refl (Fin n)

Alias of Fin.castOrderIso_refl.

theorem Fin.castOrderIso_toEquiv {m : ℕ} {n : ℕ} (h : n = m) : (Fin.castOrderIso h).toEquiv = Equiv.cast ⋯

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

@[deprecated Fin.castOrderIso_toEquiv]

theorem Fin.castIso_to_equiv {m : ℕ} {n : ℕ} (h : n = m) : (Fin.castOrderIso h).toEquiv = Equiv.cast ⋯

Alias of Fin.castOrderIso_toEquiv.

---

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

@[simp]

theorem Fin.revOrderIso_apply {n : ℕ} : ∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = (OrderDual.ofDual a).rev

@[simp]

theorem Fin.revOrderIso_toEquiv {n : ℕ} : Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm

def Fin.revOrderIso {n : ℕ} : (Fin n)ᵒᵈ ≃o Fin n

Fin.rev n as an order-reversing isomorphism.

Equations

• Fin.revOrderIso = { toEquiv := OrderDual.ofDual.trans Fin.revPerm, map_rel_iff' := ⋯ }

@[simp]

theorem Fin.revOrderIso_symm_apply {n : ℕ} (i : Fin n) : Fin.revOrderIso.symm i = OrderDual.toDual i.rev

Order embeddings

@[simp]

theorem Fin.valOrderEmb_apply (n : ℕ) (self : Fin n) : (Fin.valOrderEmb n) self = ↑self

def Fin.valOrderEmb (n : ℕ) : Fin n ↪o ℕ

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

Equations

• Fin.valOrderEmb n = { toEmbedding := Fin.valEmbedding, map_rel_iff' := ⋯ }

instance Fin.Lt.isWellOrder (n : ℕ) : IsWellOrder (Fin n) fun (x1 x2 : Fin n) => x1 < x2

The ordering on Fin n is a well order.

Equations

• ⋯ = ⋯

def Fin.succOrderEmb (n : ℕ) : Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Equations

• Fin.succOrderEmb n = OrderEmbedding.ofStrictMono Fin.succ ⋯

@[simp]

theorem Fin.coe_succOrderEmb {n : ℕ} : ⇑(Fin.succOrderEmb n) = Fin.succ

@[simp]

theorem Fin.castLEOrderEmb_apply {m : ℕ} {n : ℕ} (h : n ≤ m) (i : Fin n) : (Fin.castLEOrderEmb h) i = Fin.castLE h i

@[simp]

theorem Fin.castLEOrderEmb_toEmbedding {m : ℕ} {n : ℕ} (h : n ≤ m) : (Fin.castLEOrderEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := ⋯ }

def Fin.castLEOrderEmb {m : ℕ} {n : ℕ} (h : n ≤ m) : Fin n ↪o Fin m

Fin.castLE as an OrderEmbedding.

castLEEmb h i embeds i into a larger Fin type.

Equations

• Fin.castLEOrderEmb h = OrderEmbedding.ofStrictMono (Fin.castLE h) ⋯

@[simp]

theorem Fin.castAddOrderEmb_toEmbedding {n : ℕ} (m : ℕ) : (Fin.castAddOrderEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := ⋯ }

@[simp]

theorem Fin.castAddOrderEmb_apply {n : ℕ} (m : ℕ) : ∀ (a : Fin n), (Fin.castAddOrderEmb m) a = Fin.castAdd m a

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

• Fin.castAddOrderEmb m = OrderEmbedding.ofStrictMono (Fin.castAdd m) ⋯

@[simp]

theorem Fin.castSuccOrderEmb_toEmbedding {n : ℕ} : Fin.castSuccOrderEmb.toEmbedding = { toFun := Fin.castSucc, inj' := ⋯ }

@[simp]

theorem Fin.castSuccOrderEmb_apply {n : ℕ} : ∀ (a : Fin n), Fin.castSuccOrderEmb a = a.castSucc

def Fin.castSuccOrderEmb {n : ℕ} : Fin n ↪o Fin (n + 1)

Fin.castSucc as an OrderEmbedding.

castSuccOrderEmb i embeds i : Fin n in Fin (n+1).

Equations

• Fin.castSuccOrderEmb = OrderEmbedding.ofStrictMono Fin.castSucc ⋯

@[simp]

theorem Fin.addNatOrderEmb_apply {n : ℕ} (m : ℕ) : ∀ (x : Fin n), (Fin.addNatOrderEmb m) x = x.addNat m

@[simp]

theorem Fin.addNatOrderEmb_toEmbedding {n : ℕ} (m : ℕ) : (Fin.addNatOrderEmb m).toEmbedding = { toFun := fun (x : Fin n) => x.addNat m, inj' := ⋯ }

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

• Fin.addNatOrderEmb m = OrderEmbedding.ofStrictMono (fun (x : Fin n) => x.addNat m) ⋯

@[simp]

theorem Fin.natAddOrderEmb_toEmbedding {m : ℕ} (n : ℕ) : (Fin.natAddOrderEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := ⋯ }

@[simp]

theorem Fin.natAddOrderEmb_apply {m : ℕ} (n : ℕ) (i : Fin m) : (Fin.natAddOrderEmb n) i = Fin.natAdd n i

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

• Fin.natAddOrderEmb n = OrderEmbedding.ofStrictMono (Fin.natAdd n) ⋯

@[simp]

theorem Fin.succAboveOrderEmb_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveOrderEmb i = p.succAbove i

@[simp]

theorem Fin.succAboveOrderEmb_toEmbedding {n : ℕ} (p : Fin (n + 1)) : p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := ⋯ }

def Fin.succAboveOrderEmb {n : ℕ} (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1)

Fin.succAbove p as an OrderEmbedding.

Equations

• p.succAboveOrderEmb = OrderEmbedding.ofStrictMono p.succAbove ⋯

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

instance Fin.orderIso_subsingleton {n : ℕ} {α : Type u_1} [Preorder α] : Subsingleton (Fin n ≃o α)

Equations

• ⋯ = ⋯

instance Fin.orderIso_subsingleton' {n : ℕ} {α : Type u_1} [Preorder α] : Subsingleton (α ≃o Fin n)

Equations

• ⋯ = ⋯

instance Fin.orderIsoUnique {n : ℕ} : Unique (Fin n ≃o Fin n)

Equations

• Fin.orderIsoUnique = Unique.mk' (Fin n ≃o Fin n)

theorem Fin.strictMono_unique {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin n → α} {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.

theorem Fin.orderEmbedding_eq {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin n ↪o α} {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.