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 #

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 #

@[implicit_reducible]

instance Fin.instMax_mathlib {n : ℕ} :

@[implicit_reducible]

instance Fin.instMin_mathlib {n : ℕ} :

@[simp]

theorem Fin.coe_max {n : ℕ} (a b : Fin n) :

↑(max a b) = max ↑a ↑b

@[simp]

theorem Fin.coe_min {n : ℕ} (a b : Fin n) :

↑(min a b) = min ↑a ↑b

theorem Fin.compare_eq_compare_val {n : ℕ} (a b : Fin n) :

compare a b = compare ↑a ↑b

@[implicit_reducible]

instance Fin.instLinearOrder {n : ℕ} :

LinearOrder (Fin n)

@[implicit_reducible]

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

BoundedOrder (Fin n)

@[implicit_reducible]

instance Fin.instBiheytingAlgebra {n : ℕ} [NeZero n] :

BiheytingAlgebra (Fin n)

Extra instances to short-circuit type class resolution #

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

@[implicit_reducible]

instance Fin.instPartialOrder {n : ℕ} :

PartialOrder (Fin n)

@[implicit_reducible]

instance Fin.instLattice {n : ℕ} :

Lattice (Fin n)

@[implicit_reducible]

instance Fin.instHeytingAlgebra {n : ℕ} [NeZero n] :

HeytingAlgebra (Fin n)

@[implicit_reducible]

instance Fin.instCoheytingAlgebra {n : ℕ} [NeZero n] :

CoheytingAlgebra (Fin n)

Miscellaneous lemmas #

theorem Fin.top_eq_last (n : ℕ) :

theorem Fin.bot_eq_zero (n : ℕ) [NeZero n] :

@[simp]

theorem Fin.rev_bot {n : ℕ} [NeZero n] :

@[simp]

theorem Fin.rev_top {n : ℕ} [NeZero n] :

theorem Fin.rev_zero_eq_top (n : ℕ) [NeZero n] :

theorem Fin.rev_last_eq_bot (n : ℕ) :

(last n).rev = ⊥

@[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) :

Fin.cast h ⊤ = ⊤

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.val_strictMono {n : ℕ} :

theorem Fin.cast_strictMono {k l : ℕ} (h : k = l) :

StrictMono (Fin.cast h)

theorem Fin.strictMono_succ {n : ℕ} :

StrictMono succ

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

StrictMono (castLE h)

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

StrictMono (castAdd m)

theorem Fin.strictMono_castSucc {n : ℕ} :

StrictMono castSucc

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

StrictMono (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

@[simp]

theorem Fin.succAbove_inj {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} :

p.succAbove i = p.succAbove j ↔ i = j

@[simp]

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

p.succAbove i ≤ p.succAbove j ↔ i ≤ j

@[simp]

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

p.succAbove i < p.succAbove j ↔ i < j

@[simp]

theorem Fin.natAdd_inj {n : ℕ} (m : ℕ) {i j : Fin n} :

natAdd m i = natAdd m j ↔ i = j

theorem Fin.natAdd_injective (m n : ℕ) :

Function.Injective (natAdd n)

@[simp]

theorem Fin.natAdd_le_natAdd_iff {n : ℕ} (m : ℕ) {i j : Fin n} :

natAdd m i ≤ natAdd m j ↔ i ≤ j

@[simp]

theorem Fin.natAdd_lt_natAdd_iff {n : ℕ} (m : ℕ) {i j : Fin n} :

natAdd m i < natAdd m j ↔ i < j

@[simp]

theorem Fin.addNat_inj {n : ℕ} (m : ℕ) {i j : Fin n} :

i.addNat m = j.addNat m ↔ i = j

@[simp]

theorem Fin.addNat_le_addNat_iff {n : ℕ} (m : ℕ) {i j : Fin n} :

i.addNat m ≤ j.addNat m ↔ i ≤ j

@[simp]

theorem Fin.addNat_lt_addNat_iff {n : ℕ} (m : ℕ) {i j : Fin n} :

i.addNat m < j.addNat m ↔ i < j

@[simp]

theorem Fin.castLE_le_castLE_iff {m n : ℕ} {i j : Fin n} (h : n ≤ m) :

castLE h i ≤ castLE h j ↔ i ≤ j

@[simp]

theorem Fin.castLE_lt_castLE_iff {m n : ℕ} {i j : Fin n} (h : n ≤ m) :

castLE h i < castLE h 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

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

p.predAbove i ≤ q.predAbove j

def Fin.predAboveOrderHom {n : ℕ} (p : Fin n) :

Fin (n + 1) →o Fin n

Fin.predAbove p as an OrderHom.

Instances For

@[simp]

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

p.predAboveOrderHom i = p.predAbove i

theorem Fin.predAbove_left_injective {n : ℕ} :

Function.Injective predAbove

predAbove is injective at the pivot

@[simp]

theorem Fin.predAbove_left_inj {n : ℕ} {x y : Fin n} :

x.predAbove = y.predAbove ↔ x = y

predAbove is injective at the pivot

Order isomorphisms #

def Fin.orderIsoSubtype {n : ℕ} :

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

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

Instances For

@[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 n ≃o Fin m

Fin.cast as an OrderIso.

castOrderIso eq i embeds i into an equal Fin type.

Instances For

@[simp]

theorem Fin.castOrderIso_symm_apply {m n : ℕ} (eq : n = m) (i : Fin m) :

(RelIso.symm (castOrderIso eq)) i = Fin.cast ⋯ i

@[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) :

(castOrderIso h).symm = castOrderIso ⋯

@[simp]

theorem Fin.castOrderIso_refl {n : ℕ} (h : n = n := ⋯) :

castOrderIso h = OrderIso.refl (Fin n)

theorem Fin.castOrderIso_toEquiv {m n : ℕ} (h : n = m) :

(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.

def Fin.revOrderIso {n : ℕ} :

(Fin n)ᵒᵈ ≃o Fin n

Fin.rev n as an order-reversing isomorphism.

Instances For

@[simp]

theorem Fin.revOrderIso_toEquiv {n : ℕ} :

revOrderIso.toEquiv = OrderDual.ofDual.trans revPerm

@[simp]

theorem Fin.revOrderIso_apply {n : ℕ} (a✝ : (Fin n)ᵒᵈ) :

revOrderIso a✝ = (OrderDual.ofDual a✝).rev

@[simp]

theorem Fin.revOrderIso_symm_apply {n : ℕ} (i : Fin n) :

revOrderIso.symm i = OrderDual.toDual i.rev

theorem Fin.rev_strictAnti {n : ℕ} :

theorem Fin.rev_anti {n : ℕ} :

Order embeddings #

def Fin.valOrderEmb (n : ℕ) :

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

Instances For

@[simp]

theorem Fin.valOrderEmb_apply (n : ℕ) (self : Fin n) :

(valOrderEmb n) self = ↑self

@[implicit_reducible]

instance Fin.OrderEmbedding.instInhabitedOrderEmbeddingNat {n : ℕ} :

Inhabited (Fin n ↪o ℕ)

@[simp]

theorem Fin.OrderEmbedding.default_def {n : ℕ} :

default = valOrderEmb n

instance Fin.Lt.isWellOrder (n : ℕ) :

IsWellOrder (Fin n) fun (x1 x2 : Fin n) => x1 < x2

The ordering on Fin n is a well order.

def Fin.succOrderEmb (n : ℕ) :

Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Instances For

@[simp]

theorem Fin.coe_succOrderEmb {n : ℕ} :

⇑(succOrderEmb n) = succ

@[simp]

theorem Fin.succOrderEmb_toEmbedding {n : ℕ} :

(succOrderEmb n).toEmbedding = succEmb n

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.

Instances For

@[simp]

theorem Fin.castLEOrderEmb_toEmbedding {m n : ℕ} (h : n ≤ m) :

(castLEOrderEmb h).toEmbedding = { toFun := castLE h, inj' := ⋯ }

@[simp]

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

(castLEOrderEmb h) i = castLE h i

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.

Instances For

@[simp]

theorem Fin.castAddOrderEmb_apply {n : ℕ} (m : ℕ) (a✝ : Fin n) :

(castAddOrderEmb m) a✝ = castAdd m a✝

@[simp]

theorem Fin.castAddOrderEmb_toEmbedding {n : ℕ} (m : ℕ) :

(castAddOrderEmb m).toEmbedding = { toFun := castAdd m, inj' := ⋯ }

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

Instances For

@[simp]

theorem Fin.castSuccOrderEmb_apply {n : ℕ} (a✝ : Fin n) :

castSuccOrderEmb a✝ = a✝.castSucc

@[simp]

theorem Fin.castSuccOrderEmb_toEmbedding {n : ℕ} :

castSuccOrderEmb.toEmbedding = { toFun := castSucc, 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.

Instances For

@[simp]

theorem Fin.addNatOrderEmb_toEmbedding {n : ℕ} (m : ℕ) :

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

@[simp]

theorem Fin.addNatOrderEmb_apply {n : ℕ} (m : ℕ) (x✝ : Fin n) :

(addNatOrderEmb m) x✝ = x✝.addNat m

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".

Instances For

@[simp]

theorem Fin.natAddOrderEmb_toEmbedding {m : ℕ} (n : ℕ) :

(natAddOrderEmb n).toEmbedding = { toFun := natAdd n, inj' := ⋯ }

@[simp]

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

(natAddOrderEmb n) i = natAdd n i

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

Fin n ↪o Fin (n + 1)

Fin.succAbove p as an OrderEmbedding.

Instances For

@[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) :

p.succAboveOrderEmb i = p.succAbove i

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