The finite type with `n` elements #

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 #

Induction principles #

finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0.
Fin.succRec : Define C n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.
Fin.succRecOn : same as Fin.succRec but i : Fin n is the first argument;
Fin.induction : Define C i by induction on i : Fin (n + 1), separating into the Nat-like base cases of C 0 and C (i.succ).
Fin.inductionOn : same as Fin.induction but with i : Fin (n + 1) as the first argument.
Fin.cases : define f : Π i : Fin n.succ, C i by separately handling the cases i = 0 and i = Fin.succ j, j : Fin n, defined using Fin.induction.
Fin.reverseInduction: reverse induction on i : Fin (n + 1); given C (Fin.last n) and ∀ i : Fin n, C (Fin.succ i) → C (Fin.castSucc i), constructs all values C i by going down;
Fin.lastCases: define f : Π i, Fin (n + 1), C i by separately handling the cases i = Fin.last n and i = Fin.castSucc j, a special case of Fin.reverseInduction;
Fin.addCases: define a function on Fin (m + n) by separately handling the cases Fin.castAdd n i and Fin.natAdd m i;
Fin.succAboveCases: given i : Fin (n + 1), define a function on Fin (n + 1) by separately handling the cases j = i and j = Fin.succAbove i k, same as Fin.insertNth but marked as eliminator and works for Sort*. -- Porting note: this is in another file

Order embeddings and an order isomorphism #

Fin.orderIsoSubtype : coercion to { i // i < n } as an OrderIso;
Fin.valEmbedding : coercion to natural numbers as an Embedding;
Fin.valOrderEmbedding : coercion to natural numbers as an OrderEmbedding;
Fin.succEmbedding : Fin.succ as an OrderEmbedding;
Fin.castLEEmb h : Fin.castLE as an OrderEmbedding, embed Fin n into Fin m, h : n ≤ m;
Fin.castIso : Fin.cast as an OrderIso, order isomorphism between Fin n and Fin m provided that n = m, see also Equiv.finCongr;
Fin.castAddEmb m : Fin.castAdd as an OrderEmbedding, embed Fin n into Fin (n+m);
Fin.castSuccEmb : Fin.castSucc as an OrderEmbedding, embed Fin n into Fin (n+1);
Fin.succAboveEmb p : Fin.auccAbove as an OrderEmbedding, embed Fin n into Fin (n + 1) with a hole around p;
Fin.addNatEmb m i : Fin.addNat as an OrderEmbedding, add m on i on the right, generalizes Fin.succ;
Fin.natAddEmb n i : Fin.natAdd as an OrderEmbedding, adds n on i on the left;

Other casts #

Fin.ofNat': given a positive number n (deduced from [NeZero n]), Fin.ofNat' i is i % n interpreted as an element of Fin n;
Fin.divNat i : divides i : Fin (m * n) by n;
Fin.modNat i : takes the mod of i : Fin (m * n) by n;

Misc definitions #

Fin.revPerm : Equiv.Perm (Fin n) : Fin.rev as an Equiv.Perm, the antitone involution given by i ↦ n-(i+1)

source

def finZeroElim {α : Fin 0 → Sort u_1} (x : Fin 0) :

α x

Elimination principle for the empty set Fin 0, dependent version.

Equations

finZeroElim x = Fin.elim0 x

Instances For

source

instance Fin.instCanLiftNatFinValLtInstLTNat {n : ℕ} :

CanLift ℕ (Fin n) Fin.val fun (x : ℕ) => x < n

Equations

(_ : CanLift ℕ (Fin n) Fin.val fun (x : ℕ) => x < n) = (_ : CanLift ℕ (Fin n) Fin.val fun (x : ℕ) => x < n)

source

def Fin.elim0' {α : Sort u_1} (x : Fin 0) :

A non-dependent variant of elim0.

Equations

Fin.elim0' x = Fin.elim0 x

Instances For

source

theorem Fin.val_injective {n : ℕ} :

Function.Injective Fin.val

source

theorem Fin.size_positive {n : ℕ} :

Fin n → 0 < n

If you actually have an element of Fin n, then the n is always positive

source

theorem Fin.size_positive' {n : ℕ} [Nonempty (Fin n)] :

0 < n

source

theorem Fin.prop {n : ℕ} (a : Fin n) :

↑a < n

source

@[simp]

theorem Fin.equivSubtype_apply {n : ℕ} (a : Fin n) :

Fin.equivSubtype a = { val := ↑a, property := (_ : ↑a < n) }

source

@[simp]

theorem Fin.equivSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) :

Fin.equivSubtype.symm a = { val := ↑a, isLt := (_ : ↑a < n) }

source

def Fin.equivSubtype {n : ℕ} :

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

Equivalence between Fin n and { i // i < n }.

Equations

One or more equations did not get rendered due to their size.

Instances For

coercions and constructions #

source

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

↑a = ↑b ↔ a = b

source

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

a = b ↔ ↑a = ↑b

source

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

a ≠ b ↔ ↑a ≠ ↑b

source

@[simp]

theorem Fin.mk_eq_mk {n : ℕ} {a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} :

{ val := a, isLt := h } = { val := a', isLt := h' } ↔ a = a'

source

theorem Fin.heq_fun_iff {α : Sort u_1} {k : ℕ} {l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} :

HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < l) }

Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

source

theorem Fin.heq_fun₂_iff {α : Sort u_1} {k : ℕ} {l : ℕ} {k' : ℕ} {l' : ℕ} (h : k = l) (h' : k' = l') {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α} :

HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g { val := ↑i, isLt := (_ : ↑i < l) } { val := ↑j, isLt := (_ : ↑j < l') }

Assume k = l and k' = l'. If two functions Fin k → Fin k' → α and Fin l → Fin l' → α are equal on each pair, then they coincide (in the heq sense).

source

theorem Fin.heq_ext_iff {k : ℕ} {l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} :

HEq i j ↔ ↑i = ↑j

order #

source

theorem Fin.lt_iff_val_lt_val {n : ℕ} {a : Fin n} {b : Fin n} :

a < b ↔ ↑a < ↑b

source

theorem Fin.le_iff_val_le_val {n : ℕ} {a : Fin n} {b : Fin n} :

a ≤ b ↔ ↑a ≤ ↑b

source

@[simp]

theorem Fin.val_fin_lt {n : ℕ} {a : Fin n} {b : Fin n} :

↑a < ↑b ↔ a < b

a < b as natural numbers if and only if a < b in Fin n.

source

@[simp]

theorem Fin.val_fin_le {n : ℕ} {a : Fin n} {b : Fin n} :

↑a ≤ ↑b ↔ a ≤ b

a ≤ b as natural numbers if and only if a ≤ b in Fin n.

source

instance Fin.instLinearOrderFin {n : ℕ} :

LinearOrder (Fin n)

Equations

One or more equations did not get rendered due to their size.

source

theorem Fin.min_val {n : ℕ} {a : Fin n} :

min (↑a) n = ↑a

source

theorem Fin.max_val {n : ℕ} {a : Fin n} :

max (↑a) n = n

source

instance Fin.instPartialOrderFin {n : ℕ} :

PartialOrder (Fin n)

Equations

Fin.instPartialOrderFin = inferInstance

source

theorem Fin.val_strictMono {n : ℕ} :

StrictMono Fin.val

source

@[simp]

theorem Fin.orderIsoSubtype_apply {n : ℕ} (a : Fin n) :

Fin.orderIsoSubtype a = { val := ↑a, property := (_ : ↑a < n) }

source

@[simp]

theorem Fin.orderIsoSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) :

(RelIso.symm Fin.orderIsoSubtype) a = { val := ↑a, isLt := (_ : ↑a < n) }

source

def Fin.orderIsoSubtype {n : ℕ} :

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

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Fin.valEmbedding_apply {n : ℕ} (self : Fin n) :

Fin.valEmbedding self = ↑self

source

def Fin.valEmbedding {n : ℕ} :

Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

Fin.valEmbedding = { toFun := Fin.val, inj' := (_ : Function.Injective Fin.val) }

Instances For

source

@[simp]

theorem Fin.equivSubtype_symm_trans_valEmbedding {n : ℕ} :

Function.Embedding.trans (Equiv.toEmbedding Fin.equivSubtype.symm) Fin.valEmbedding = Function.Embedding.subtype fun (x : ℕ) => x < n

source

@[simp]

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

(Fin.valOrderEmbedding n) self = ↑self

source

def Fin.valOrderEmbedding (n : ℕ) :

Fin n ↪o ℕ

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

Equations

Fin.valOrderEmbedding n = { toEmbedding := Fin.valEmbedding, map_rel_iff' := (_ : ∀ {a b : Fin n}, Fin.valEmbedding a ≤ Fin.valEmbedding b ↔ Fin.valEmbedding a ≤ Fin.valEmbedding b) }

Instances For

source

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

IsWellOrder (Fin n) fun (x x_1 : Fin n) => x < x_1

The ordering on Fin n is a well order.

Equations

(_ : IsWellOrder (Fin n) fun (x x_1 : Fin n) => x < x_1) = (_ : IsWellOrder (Fin n) fun (x x_1 : Fin n) => x < x_1)

source

instance Fin.instWellFoundedRelationFin {n : ℕ} :

WellFoundedRelation (Fin n)

Use the ordering on Fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the WellFoundedRelation instance:

def factorial {n : ℕ} : Fin n → ℕ
  | ⟨0, _⟩ := 1
  | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

Equations

Fin.instWellFoundedRelationFin = measure Fin.val

source

def Fin.ofNat'' {n : ℕ} [NeZero n] (i : ℕ) :

Fin n

Given a positive n, Fin.ofNat' i is i % n as an element of Fin n.

Equations

Fin.ofNat'' i = { val := i % n, isLt := (_ : i % n < n) }

Instances For

source

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

Zero (Fin n)

Equations

Fin.instZeroFin = { zero := Fin.ofNat'' 0 }

source

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

One (Fin n)

Equations

Fin.instOneFin = { one := Fin.ofNat'' 1 }

source

@[simp]

theorem Fin.val_zero' (n : ℕ) [NeZero n] :

↑0 = 0

The Fin.val_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

@[simp]

theorem Fin.zero_le' {n : ℕ} [NeZero n] (a : Fin n) :

0 ≤ a

The Fin.zero_le in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

theorem Fin.pos_iff_ne_zero' {n : ℕ} [NeZero n] (a : Fin n) :

0 < a ↔ a ≠ 0

The Fin.pos_iff_ne_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

theorem Fin.rev_involutive {n : ℕ} :

Function.Involutive Fin.rev

source

@[simp]

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

Fin.revPerm.symm i = Fin.rev i

source

@[simp]

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

Fin.revPerm i = Fin.rev i

source

def Fin.revPerm {n : ℕ} :

Equiv.Perm (Fin n)

Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by i ↦ n-(i+1).

Equations

Fin.revPerm = Function.Involutive.toPerm Fin.rev (_ : Function.Involutive Fin.rev)

Instances For

source

theorem Fin.rev_injective {n : ℕ} :

Function.Injective Fin.rev

source

theorem Fin.rev_surjective {n : ℕ} :

Function.Surjective Fin.rev

source

theorem Fin.rev_bijective {n : ℕ} :

Function.Bijective Fin.rev

source

@[simp]

theorem Fin.revPerm_symm {n : ℕ} :

Fin.revPerm.symm = Fin.revPerm

source

@[simp]

theorem Fin.revOrderIso_toEquiv {n : ℕ} :

Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm

source

@[simp]

theorem Fin.revOrderIso_apply {n : ℕ} :

∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = Fin.rev (OrderDual.ofDual a)

source

def Fin.revOrderIso {n : ℕ} :

(Fin n)ᵒᵈ ≃o Fin n

Fin.rev n as an order-reversing isomorphism.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

(OrderIso.symm Fin.revOrderIso) i = OrderDual.toDual (Fin.rev i)

source

instance Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin {n : ℕ} :

BoundedOrder (Fin (n + 1))

Equations

Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin = BoundedOrder.mk

source

instance Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat {n : ℕ} :

Lattice (Fin (n + 1))

Equations

Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat = LinearOrder.toLattice

source

theorem Fin.top_eq_last (n : ℕ) :

⊤ = Fin.last n

source

theorem Fin.bot_eq_zero (n : ℕ) :

⊥ = 0

source

@[simp]

theorem Fin.coe_orderIso_apply {n : ℕ} {m : ℕ} (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 : ℕ).

source

instance Fin.orderIso_subsingleton {n : ℕ} {α : Type u_1} [Preorder α] :

Subsingleton (Fin n ≃o α)

Equations

(_ : Subsingleton (Fin n ≃o α)) = (_ : Subsingleton (Fin n ≃o α))

source

instance Fin.orderIso_subsingleton' {n : ℕ} {α : Type u_1} [Preorder α] :

Subsingleton (α ≃o Fin n)

Equations

(_ : Subsingleton (α ≃o Fin n)) = (_ : Subsingleton (α ≃o Fin n))

source

instance Fin.orderIsoUnique {n : ℕ} :

Unique (Fin n ≃o Fin n)

Equations

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

source

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.

source

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.

addition, numerals, and coercion from Nat #

source

@[simp]

theorem Fin.val_one' (n : ℕ) [NeZero n] :

↑1 = 1 % n

source

theorem Fin.val_one'' {n : ℕ} :

↑1 = 1 % (n + 1)

source

instance Fin.nontrivial {n : ℕ} :

Nontrivial (Fin (n + 2))

Equations

(_ : Nontrivial (Fin (n + 2))) = (_ : Nontrivial (Fin (n + 2)))

source

theorem Fin.nontrivial_iff_two_le {n : ℕ} :

Nontrivial (Fin n) ↔ 2 ≤ n

source

instance Fin.addCommSemigroup (n : ℕ) :

AddCommSemigroup (Fin n)

Equations

One or more equations did not get rendered due to their size.

source

theorem Fin.add_zero {n : ℕ} [NeZero n] (k : Fin n) :

k + 0 = k

source

theorem Fin.zero_add {n : ℕ} [NeZero n] (k : Fin n) :

0 + k = k

source

instance Fin.instOfNatFin {n : ℕ} {a : ℕ} [NeZero n] :

OfNat (Fin n) a

Equations

Fin.instOfNatFin = { ofNat := Fin.ofNat' a (_ : 0 < n) }

source

instance Fin.inhabited (n : ℕ) [NeZero n] :

Inhabited (Fin n)

Equations

Fin.inhabited n = { default := 0 }

source

instance Fin.inhabitedFinOneAdd (n : ℕ) :

Inhabited (Fin (1 + n))

Equations

Fin.inhabitedFinOneAdd n = inferInstance

source

@[simp]

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

default = 0

source

@[simp]

theorem Fin.ofNat'_zero {n : ℕ} {h : n > 0} [NeZero n] :

Fin.ofNat' 0 h = 0

source

@[simp]

theorem Fin.ofNat'_one {n : ℕ} {h : n > 0} [NeZero n] :

Fin.ofNat' 1 h = 1

source

instance Fin.instAddCommSemigroupFin (n : ℕ) :

AddCommSemigroup (Fin n)

Equations

Fin.instAddCommSemigroupFin n = AddCommSemigroup.mk (_ : ∀ (a a_1 : Fin n), { val := (↑a + ↑a_1) % n, isLt := (_ : (↑a + ↑a_1) % n < n) } = a_1 + a)

source

instance Fin.addCommMonoid (n : ℕ) [NeZero n] :

AddCommMonoid (Fin n)

Equations

Fin.addCommMonoid n = let src := Fin.addCommSemigroup n; AddCommMonoid.mk (_ : ∀ (a b : Fin n), a + b = b + a)

source

instance Fin.instAddMonoidWithOne (n : ℕ) [NeZero n] :

AddMonoidWithOne (Fin n)

Equations

Fin.instAddMonoidWithOne n = let src := inferInstanceAs (AddCommMonoid (Fin n)); AddMonoidWithOne.mk

source

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

↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

source

@[deprecated]

theorem Fin.val_bit0 {n : ℕ} (k : Fin n) :

↑(bit0 k) = bit0 ↑k % n

source

@[deprecated]

theorem Fin.val_bit1 {n : ℕ} [NeZero n] (k : Fin n) :

↑(bit1 k) = bit1 ↑k % n

source

@[simp, deprecated]

theorem Fin.mk_bit0 {m : ℕ} {n : ℕ} (h : bit0 m < n) :

{ val := bit0 m, isLt := h } = bit0 { val := m, isLt := (_ : m < n) }

source

@[simp, deprecated]

theorem Fin.mk_bit1 {m : ℕ} {n : ℕ} [NeZero n] (h : bit1 m < n) :

{ val := bit1 m, isLt := h } = bit1 { val := m, isLt := (_ : m < n) }

source

@[simp]

theorem Fin.ofNat_eq_val (n : ℕ) [NeZero n] (a : ℕ) :

Fin.ofNat'' a = ↑a

source

theorem Fin.val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) :

↑↑a = a

Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

source

theorem Fin.cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) :

↑↑a = a

Converting the value of a Fin (n + 1) to Fin (n + 1) results in the same value.

source

theorem Fin.cast_nat_eq_last (n : ℕ) :

↑n = Fin.last n

source

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

i ≤ ↑n

source

@[simp]

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

0 = 1 ↔ n = 1

source

@[simp]

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

1 = 0 ↔ n = 1

succ and casts into larger Fin types #

source

def Fin.succEmbedding (n : ℕ) :

Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Equations

Fin.succEmbedding n = OrderEmbedding.ofStrictMono Fin.succ (_ : ∀ (x x_1 : Fin n), x < x_1 → Nat.succ ↑x < Nat.succ ↑x_1)

Instances For

source

@[simp]

theorem Fin.val_succEmbedding {n : ℕ} :

⇑(Fin.succEmbedding n) = Fin.succ

source

theorem Fin.succ_injective (n : ℕ) :

Function.Injective Fin.succ

source

@[simp]

theorem Fin.succ_zero_eq_one' {n : ℕ} [NeZero n] :

Fin.succ 0 = 1

source

@[simp]

theorem Fin.succ_one_eq_two' {n : ℕ} [NeZero n] :

Fin.succ 1 = 2

The Fin.succ_one_eq_two in Std only applies in Fin (n+2). This one instead uses a NeZero n typeclass hypothesis.

source

@[simp]

theorem Fin.le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} :

k ≤ 0 ↔ k = 0

The Fin.le_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

@[simp]

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

Fin.cast h = id

source

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

StrictMono (Fin.castLE h)

source

@[simp]

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

(Fin.castLEEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := (_ : ∀ (x x_1 : Fin n), Fin.castLE h x = Fin.castLE h x_1 → x = x_1) }

source

@[simp]

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

(Fin.castLEEmb h) i = Fin.castLE h i

source

def Fin.castLEEmb {n : ℕ} {m : ℕ} (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.castLEEmb h = OrderEmbedding.ofStrictMono (Fin.castLE h) (_ : StrictMono (Fin.castLE h))

Instances For

source

@[simp]

theorem Fin.castLE_castSucc {n : ℕ} {m : ℕ} (i : Fin n) (h : n + 1 ≤ m) :

Fin.castLE h (Fin.castSucc i) = Fin.castLE (_ : n ≤ m) i

source

@[simp]

theorem Fin.castLE_comp_castSucc {n : ℕ} {m : ℕ} (h : n + 1 ≤ m) :

Fin.castLE h ∘ Fin.castSucc = Fin.castLE (_ : n ≤ m)

source

@[simp]

theorem Fin.castLE_rfl (n : ℕ) :

Fin.castLE (_ : n ≤ n) = id

source

@[simp]

theorem Fin.range_castLE {n : ℕ} {k : ℕ} (h : n ≤ k) :

Set.range (Fin.castLE h) = {i : Fin k | ↑i < n}

source

@[simp]

theorem Fin.coe_of_injective_castLEEmb_symm {n : ℕ} {k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range ⇑(Fin.castLEEmb h)) :

↑((Equiv.ofInjective ⇑(Fin.castLEEmb h) (_ : Function.Injective ⇑(Fin.castLEEmb h))).symm { val := i, property := hi }) = ↑i

source

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

Function.LeftInverse (Fin.cast (_ : m = n)) (Fin.cast eq)

source

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

Function.RightInverse (Fin.cast (_ : m = n)) (Fin.cast eq)

source

theorem Fin.cast_le_cast {n : ℕ} {m : ℕ} (eq : n = m) {a : Fin n} {b : Fin n} :

Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b

source

@[simp]

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

(RelIso.symm (Fin.castIso eq)) i = Fin.cast (_ : m = n) i

source

@[simp]

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

(Fin.castIso eq) i = Fin.cast eq i

source

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

Fin n ≃o Fin m

Fin.cast as an OrderIso, castIso eq i embeds i into an equal Fin type, see also Equiv.finCongr.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

OrderIso.symm (Fin.castIso h) = Fin.castIso (_ : m = n)

source

@[simp]

theorem Fin.cast_zero {n : ℕ} {n' : ℕ} [NeZero n] {h : n = n'} :

Fin.cast h 0 = 0

source

@[simp]

theorem Fin.castIso_refl {n : ℕ} (h : optParam (n = n) (_ : n = n)) :

Fin.castIso h = OrderIso.refl (Fin n)

source

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

(Fin.castIso h).toEquiv = Equiv.cast (_ : Fin n = Fin m)

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

source

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

Fin.cast h = cast (_ : Fin n = Fin m)

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

source

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

StrictMono (Fin.castAdd m)

source

@[simp]

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

(Fin.castAddEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := (_ : ∀ (x x_1 : Fin n), Fin.castAdd m x = Fin.castAdd m x_1 → x = x_1) }

source

@[simp]

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

∀ (a : Fin n), (Fin.castAddEmb m) a = Fin.castAdd m a

source

def Fin.castAddEmb {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.castAddEmb m = OrderEmbedding.ofStrictMono (Fin.castAdd m) (_ : StrictMono (Fin.castAdd m))

Instances For

source

theorem Fin.strictMono_castSucc {n : ℕ} :

StrictMono Fin.castSucc

source

@[simp]

theorem Fin.castSuccEmb_apply {n : ℕ} :

∀ (a : Fin n), Fin.castSuccEmb a = Fin.castSucc a

source

@[simp]

theorem Fin.castSuccEmb_toEmbedding {n : ℕ} :

Fin.castSuccEmb.toEmbedding = { toFun := Fin.castSucc, inj' := (_ : ∀ (x x_1 : Fin n), Fin.castSucc x = Fin.castSucc x_1 → x = x_1) }

source

def Fin.castSuccEmb {n : ℕ} :

Fin n ↪o Fin (n + 1)

Fin.castSucc as an OrderEmbedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

Equations

Fin.castSuccEmb = OrderEmbedding.ofStrictMono Fin.castSucc (_ : StrictMono Fin.castSucc)

Instances For

source

theorem Fin.castSucc_injective (n : ℕ) :

Function.Injective Fin.castSucc

source

@[simp]

theorem Fin.castSucc_zero' {n : ℕ} [NeZero n] :

Fin.castSucc 0 = 0

The Fin.castSucc_zero in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

theorem Fin.castSucc_pos' {n : ℕ} [NeZero n] {i : Fin n} (h : 0 < i) :

0 < Fin.castSucc i

castSucc i is positive when i is positive.

The Fin.castSucc_pos in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

@[simp]

theorem Fin.castSucc_eq_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) :

Fin.castSucc a = 0 ↔ a = 0

The Fin.castSucc_eq_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

theorem Fin.castSucc_ne_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) :

Fin.castSucc a ≠ 0 ↔ a ≠ 0

The Fin.castSucc_ne_zero_iff in Std only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

source

@[simp]

theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} :

↑↑a = Fin.castSucc a

source

@[simp]

theorem Fin.range_castSucc {n : ℕ} :

Set.range Fin.castSucc = {i : Fin (Nat.succ n) | ↑i < n}

source

@[simp]

theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin (Nat.succ n)) (hi : i ∈ Set.range Fin.castSucc) :

↑((Equiv.ofInjective Fin.castSucc (_ : Function.Injective Fin.castSucc)).symm { val := i, property := hi }) = ↑i

source

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

StrictMono fun (x : Fin n) => Fin.addNat x m

source

@[simp]

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

∀ (x : Fin n), (Fin.addNatEmb m) x = Fin.addNat x m

source

@[simp]

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

(Fin.addNatEmb m).toEmbedding = { toFun := fun (x : Fin n) => Fin.addNat x m, inj' := (_ : ∀ (x x_1 : Fin n), Fin.addNat x m = Fin.addNat x_1 m → x = x_1) }

source

def Fin.addNatEmb {n : ℕ} (m : ℕ) :

Fin n ↪o Fin (n + m)

Fin.addNat as an OrderEmbedding, addNatEmb m i adds m to i, generalizes Fin.succ.

Equations

Fin.addNatEmb m = OrderEmbedding.ofStrictMono (fun (x : Fin n) => Fin.addNat x m) (_ : StrictMono fun (x : Fin n) => Fin.addNat x m)

Instances For

source

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

StrictMono (Fin.natAdd n)

source

@[simp]

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

(Fin.natAddEmb n) i = Fin.natAdd n i

source

@[simp]

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

(Fin.natAddEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := (_ : ∀ (x x_1 : Fin m), Fin.natAdd n x = Fin.natAdd n x_1 → x = x_1) }

source

def Fin.natAddEmb (n : ℕ) {m : ℕ} :

Fin m ↪o Fin (n + m)

Fin.natAdd as an OrderEmbedding, natAddEmb n i adds n to i "on the left".

Equations

Fin.natAddEmb n = OrderEmbedding.ofStrictMono (Fin.natAdd n) (_ : StrictMono (Fin.natAdd n))

Instances For

pred #

source

def Fin.divNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

Fin m

Compute i / n, where n is a Nat and inferred the type of i.

Equations

Fin.divNat i = { val := ↑i / n, isLt := (_ : ↑i / n < m) }

Instances For

source

@[simp]

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

↑(Fin.divNat i) = ↑i / n

source

def Fin.modNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

Fin n

Compute i % n, where n is a Nat and inferred the type of i.

Equations

Fin.modNat i = { val := ↑i % n, isLt := (_ : ↑i % n < n) }

Instances For

source

@[simp]

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

↑(Fin.modNat i) = ↑i % n

recursion and induction principles #

source

theorem Fin.liftFun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} :

((fun (x x_1 : Fin (n + 1)) => x < x_1) ⇒ r) f f ↔ ∀ (i : Fin n), r (f (Fin.castSucc i)) (f (Fin.succ i))

source

theorem Fin.strictMono_iff_lt_succ {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} :

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

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

source

theorem Fin.monotone_iff_le_succ {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} :

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

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

source

theorem Fin.strictAnti_iff_succ_lt {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} :

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

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

source

theorem Fin.antitone_iff_succ_le {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} :

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

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

source

instance Fin.neg (n : ℕ) :

Neg (Fin n)

Negation on Fin n

Equations

Fin.neg n = { neg := fun (a : Fin n) => { val := (n - ↑a) % n, isLt := (_ : (n - ↑a) % n < n) } }

source

instance Fin.addCommGroup (n : ℕ) [NeZero n] :

AddCommGroup (Fin n)

Abelian group structure on Fin n.

Equations

Fin.addCommGroup n = let src := Fin.addCommMonoid n; let src_1 := Fin.neg n; AddCommGroup.mk (_ : ∀ (a b : Fin n), a + b = b + a)

source

instance Fin.instInvolutiveNeg (n : ℕ) :

InvolutiveNeg (Fin n)

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Fin.instInvolutiveNeg n = InvolutiveNeg.mk (_ : ∀ (x : Fin n), - -x = x)

source

instance Fin.instIsCancelAdd (n : ℕ) :

IsCancelAdd (Fin n)

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

(_ : IsCancelAdd (Fin n)) = (_ : IsCancelAdd (Fin n))

source

instance Fin.instAddLeftCancelSemigroup (n : ℕ) :

AddLeftCancelSemigroup (Fin n)

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Fin.instAddLeftCancelSemigroup n = let src := Fin.addCommSemigroup n; let src_1 := (_ : IsCancelAdd (Fin n)); AddLeftCancelSemigroup.mk (_ : ∀ (a b c : Fin n), a + b = a + c → b = c)

source

instance Fin.instAddRightCancelSemigroup (n : ℕ) :

AddRightCancelSemigroup (Fin n)

Note this is more general than Fin.addCommGroup as it applies (vacuously) to Fin 0 too.

Equations

Fin.instAddRightCancelSemigroup n = let src := Fin.addCommSemigroup n; let src_1 := (_ : IsCancelAdd (Fin n)); AddRightCancelSemigroup.mk (_ : ∀ (a b c : Fin n), a + b = c + b → a = c)

source

theorem Fin.coe_neg {n : ℕ} (a : Fin n) :

↑(-a) = (n - ↑a) % n

source

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

↑(a - b) = (↑a + (n - ↑b)) % n

source

theorem Fin.eq_zero (n : Fin 1) :

n = 0

source

instance Fin.uniqueFinOne :

Unique (Fin 1)

Equations

Fin.uniqueFinOne = { toInhabited := Fin.inhabited 1, uniq := Fin.uniqueFinOne.proof_2 }

source

@[simp]

theorem Fin.coe_fin_one (a : Fin 1) :

↑a = 0

source

theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) :

i = 1

source

@[simp]

theorem Fin.coe_neg_one {n : ℕ} :

↑(-1) = n

source

theorem Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) :

↑(a - 1) = if a = 0 then n else ↑a - 1

source

theorem Fin.coe_sub_iff_le {n : ℕ} {a : Fin n} {b : Fin n} :

↑(a - b) = ↑a - ↑b ↔ b ≤ a

source

theorem Fin.coe_sub_iff_lt {n : ℕ} {a : Fin n} {b : Fin n} :

↑(a - b) = n + ↑a - ↑b ↔ a < b

source

@[simp]

theorem Fin.lt_sub_one_iff {n : ℕ} {k : Fin (n + 2)} :

k < k - 1 ↔ k = 0

source

@[simp]

theorem Fin.le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} :

k ≤ k - 1 ↔ k = 0

source

@[simp]

theorem Fin.sub_one_lt_iff {n : ℕ} {k : Fin (n + 1)} :

k - 1 < k ↔ 0 < k

source

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

Fin.last n - i = Fin.rev i

source

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

Fin (n + 1)

succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.

Equations

Fin.succAbove p i = if ↑i < ↑p then Fin.castSucc i else Fin.succ i

Instances For

source

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

StrictMono (Fin.succAbove p)

source

@[simp]

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

(Fin.succAboveEmb p).toEmbedding = { toFun := Fin.succAbove p, inj' := (_ : ∀ (x x_1 : Fin n), Fin.succAbove p x = Fin.succAbove p x_1 → x = x_1) }

source

@[simp]

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

(Fin.succAboveEmb p) i = Fin.succAbove p i

source

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

Fin n ↪o Fin (n + 1)

Fin.auccAbove as an OrderEmbedding, succAboveEmb p i embeds Fin n into Fin (n + 1) with a hole around p.

Equations

Fin.succAboveEmb p = OrderEmbedding.ofStrictMono (Fin.succAbove p) (_ : StrictMono (Fin.succAbove p))

Instances For

source

theorem Fin.succAbove_below {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : Fin.castSucc i < p) :

Fin.succAbove p i = Fin.castSucc i

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by castSucc when the resulting i.castSucc < p.

source

@[simp]

theorem Fin.succAbove_ne_zero_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) :

Fin.succAbove a 0 = 0

source

theorem Fin.succAbove_eq_zero_iff {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) :

Fin.succAbove a b = 0 ↔ b = 0

source

theorem Fin.succAbove_ne_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) (hb : b ≠ 0) :

Fin.succAbove a b ≠ 0

source

@[simp]

theorem Fin.succAbove_zero {n : ℕ} :

Fin.succAbove 0 = Fin.succ

Embedding Fin n into Fin (n + 1) with a hole around zero embeds by succ.

source

@[simp]

theorem Fin.succAbove_last {n : ℕ} :

Fin.succAbove (Fin.last n) = Fin.castSucc

Embedding Fin n into Fin (n + 1) with a hole around last n embeds by castSucc.

source

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

Fin.succAbove (Fin.last n) i = Fin.castSucc i

source

theorem Fin.succAbove_above {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ Fin.castSucc i) :

Fin.succAbove p i = Fin.succ i

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by succ when the resulting p < i.succ.

source

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

Fin.castSucc i < p ∨ p ≤ Fin.castSucc i

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

source

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

Fin.castSucc i < p ∨ p < Fin.succ i

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

source

@[simp]

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

Fin.succAbove p i < p ↔ Fin.castSucc i < p

Embedding i : Fin n into Fin (n + 1) using a pivot p that is greater results in a value that is less than p.

source

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

p < Fin.succAbove p i ↔ p ≤ Fin.castSucc i

Embedding i : Fin n into Fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

source

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

Fin.succAbove p i ≠ p

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) never results in p itself

source

theorem Fin.succAbove_pos {n : ℕ} [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) :

0 < Fin.succAbove p i

Embedding a positive Fin n results in a positive Fin (n + 1)

source

@[simp]

theorem Fin.succAbove_castLT {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hx : optParam (↑x < n) (_ : ↑x < n)) :

Fin.succAbove y (Fin.castLT x hx) = x

source

@[simp]

theorem Fin.succAbove_pred {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hy : optParam (y ≠ 0) (_ : y ≠ 0)) :

Fin.succAbove x (Fin.pred y hy) = y

source

theorem Fin.castLT_succAbove {n : ℕ} {x : Fin n} {y : Fin (n + 1)} (h : Fin.castSucc x < y) (h' : optParam (↑(Fin.succAbove y x) < n) (_ : ↑(Fin.succAbove y x) < n)) :

Fin.castLT (Fin.succAbove y x) h' = x

source

theorem Fin.pred_succAbove {n : ℕ} {x : Fin n} {y : Fin (n + 1)} (h : y ≤ Fin.castSucc x) (h' : optParam (Fin.succAbove y x ≠ 0) (_ : Fin.succAbove y x ≠ 0)) :

Fin.pred (Fin.succAbove y x) h' = x

source

theorem Fin.exists_succAbove_eq {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x ≠ y) :

∃ (z : Fin n), Fin.succAbove y z = x

source

@[simp]

theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} :

(∃ (z : Fin n), Fin.succAbove x z = y) ↔ y ≠ x

source

@[simp]

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

Set.range (Fin.succAbove p) = {p}ᶜ

The range of p.succAbove is everything except p.

source

@[simp]

theorem Fin.range_succ (n : ℕ) :

Set.range Fin.succ = {0}ᶜ

source

@[simp]

theorem Fin.exists_succ_eq_iff {n : ℕ} {x : Fin (n + 1)} :

(∃ (y : Fin n), Fin.succ y = x) ↔ x ≠ 0

source

theorem Fin.succAbove_right_injective {n : ℕ} {x : Fin (n + 1)} :

Function.Injective (Fin.succAbove x)

Given a fixed pivot x : Fin (n + 1), x.succAbove is injective

source

theorem Fin.succAbove_right_inj {n : ℕ} {a : Fin n} {b : Fin n} {x : Fin (n + 1)} :

Fin.succAbove x a = Fin.succAbove x b ↔ a = b

Given a fixed pivot x : Fin (n + 1), x.succAbove is injective

source

theorem Fin.succAbove_left_injective {n : ℕ} :

Function.Injective Fin.succAbove

succAbove is injective at the pivot

source

@[simp]

theorem Fin.succAbove_left_inj {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} :

Fin.succAbove x = Fin.succAbove y ↔ x = y

succAbove is injective at the pivot

source

@[simp]

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

Fin.succAbove 0 i = Fin.succ i

source

@[simp]

theorem Fin.succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) :

Fin.succAbove (Fin.succ i) 0 = 0

source

@[simp]

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

Fin.succAbove (Fin.succ i) (Fin.succ j) = Fin.succ (Fin.succAbove i j)

source

theorem Fin.one_succAbove_zero {n : ℕ} :

Fin.succAbove 1 0 = 0

source

@[simp]

theorem Fin.succ_succAbove_one {n : ℕ} [NeZero n] (i : Fin (n + 1)) :

Fin.succAbove (Fin.succ i) 1 = Fin.succ (Fin.succAbove i 0)

By moving succ to the outside of this expression, we create opportunities for further simplification using succAbove_zero or succ_succAbove_zero.

source

@[simp]

theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) :

Fin.succAbove 1 (Fin.succ j) = Fin.succ (Fin.succ j)

source

@[simp]

theorem Fin.one_succAbove_one {n : ℕ} :

Fin.succAbove 1 1 = 2

source

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

Fin n

predAbove p i embeds i : Fin (n+1) into Fin n by subtracting one if p < i.

Equations

Fin.predAbove p i = if h : Fin.castSucc p < i then Fin.pred i (_ : i ≠ 0) else Fin.castLT i (_ : ↑i < n)

Instances For

source

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

Monotone (Fin.predAbove p)

source

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

Monotone fun (p : Fin n) => Fin.predAbove p i

source

def Fin.castPred {n : ℕ} (i : Fin (n + 2)) :

Fin (n + 1)

castPred embeds i : Fin (n + 2) into Fin (n + 1) by lowering just last (n + 1) to last n.

Equations

Fin.castPred i = Fin.predAbove (Fin.last n) i

Instances For

source

@[simp]

theorem Fin.castPred_zero {n : ℕ} :

Fin.castPred 0 = 0

source

@[simp]

theorem Fin.castPred_one {n : ℕ} :

Fin.castPred 1 = 1

source

@[simp]

theorem Fin.predAbove_zero {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ 0) :

Fin.predAbove 0 i = Fin.pred i hi

source

@[simp]

theorem Fin.castPred_last {n : ℕ} :

Fin.castPred (Fin.last (n + 1)) = Fin.last n

source

theorem Fin.castPred_mk (n : ℕ) (i : ℕ) (h : i < n + 1) :

Fin.castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }

source

@[simp]

theorem Fin.castPred_mk' (n : ℕ) (i : ℕ) (h₁ : i < n + 2) (h₂ : i < n + 1) :

Fin.castPred { val := i, isLt := h₁ } = { val := i, isLt := h₂ }

source

theorem Fin.coe_castPred {n : ℕ} (a : Fin (n + 2)) (hx : a < Fin.last (n + 1)) :

↑(Fin.castPred a) = ↑a

source

theorem Fin.predAbove_below {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 2)) (h : i ≤ Fin.castSucc p) :

Fin.predAbove p i = Fin.castPred i

source

@[simp]

theorem Fin.predAbove_last {n : ℕ} :

Fin.predAbove (Fin.last n) = Fin.castPred

source

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

Fin.predAbove (Fin.last n) ↑↑i = Fin.castPred ↑↑i

source

theorem Fin.predAbove_above {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : Fin.castSucc p < i) :

Fin.predAbove p i = Fin.pred i (_ : i ≠ 0)

source

theorem Fin.castPred_monotone {n : ℕ} :

Monotone Fin.castPred

source

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ Fin.castSucc p) :

Fin.succAbove (Fin.castSucc p) (Fin.predAbove p i) = i

Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p is the identity away from p.

source

@[simp]