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

Embeddings and isomorphisms

• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.succEmb : Fin.succ as an Embedding;
• Fin.castLEEmb h : Fin.castLE as an Embedding, embed Fin n into Fin m, h : n ≤ m;
• finCongr : Fin.cast as an Equiv, equivalence between Fin n and Fin m when n = m;
• Fin.castAddEmb m : Fin.castAdd as an Embedding, embed Fin n into Fin (n+m);
• Fin.castSuccEmb : Fin.castSucc as an Embedding, embed Fin n into Fin (n+1);
• Fin.addNatEmb m i : Fin.addNat as an Embedding, add m on i on the right, generalizes Fin.succ;
• Fin.natAddEmb n i : Fin.natAdd as an Embedding, 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)

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

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

Equations

• finZeroElim x = x.elim0

@[deprecated Fin.eq_of_val_eq]

theorem Fin.eq_of_veq {n : ℕ} {i j : Fin n} : ↑i = ↑j → i = j

Alias of Fin.eq_of_val_eq.

@[deprecated Fin.val_eq_of_eq]

theorem Fin.veq_of_eq {n : ℕ} {i j : Fin n} (h : i = j) : ↑i = ↑j

Alias of Fin.val_eq_of_eq.

@[deprecated Fin.ne_of_val_ne]

theorem Fin.ne_of_vne {n : ℕ} {i j : Fin n} (h : ↑i ≠ ↑j) : i ≠ j

Alias of Fin.ne_of_val_ne.

@[deprecated Fin.val_ne_of_ne]

theorem Fin.vne_of_ne {n : ℕ} {i j : Fin n} (h : i ≠ j) : ↑i ≠ ↑j

Alias of Fin.val_ne_of_ne.

theorem Fin.instCanLiftNatValLt {n : ℕ} : CanLift ℕ (Fin n) Fin.val fun (x : ℕ) => x < n

def Fin.rec0 {α : Fin 0 → Sort u_1} (i : Fin 0) : α i

A dependent variant of Fin.elim0.

Equations

• i.rec0 = absurd ⋯ ⋯

theorem Fin.val_injective {n : ℕ} : Function.Injective Fin.val

theorem Fin.size_positive {n : ℕ} : Fin n → 0 < n

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

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

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

theorem Fin.lt_of_le_of_lt {n : ℕ} {a b c : Fin n} : a ≤ b → b < c → a < c

theorem Fin.lt_of_lt_of_le {n : ℕ} {a b c : Fin n} : a < b → b ≤ c → a < c

theorem Fin.le_rfl {n : ℕ} {a : Fin n} : a ≤ a

theorem Fin.lt_iff_le_and_ne {n : ℕ} {a b : Fin n} : a < b ↔ a ≤ b ∧ a ≠ b

theorem Fin.lt_or_lt_of_ne {n : ℕ} {a b : Fin n} (h : a ≠ b) : a < b ∨ b < a

theorem Fin.lt_or_le {n : ℕ} (a b : Fin n) : a < b ∨ b ≤ a

theorem Fin.le_or_lt {n : ℕ} (a b : Fin n) : a ≤ b ∨ b < a

theorem Fin.le_of_eq {n : ℕ} {a b : Fin n} (hab : a = b) : a ≤ b

theorem Fin.ge_of_eq {n : ℕ} {a b : Fin n} (hab : a = b) : b ≤ a

theorem Fin.eq_or_lt_of_le {n : ℕ} {a b : Fin n} : a ≤ b → a = b ∨ a < b

theorem Fin.lt_or_eq_of_le {n : ℕ} {a b : Fin n} : a ≤ b → a < b ∨ a = b

theorem Fin.lt_last_iff_ne_last {n : ℕ} {a : Fin (n + 1)} : a < Fin.last n ↔ a ≠ Fin.last n

theorem Fin.ne_zero_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : b ≠ 0

theorem Fin.ne_last_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : a ≠ Fin.last n

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

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

Equations

• Fin.equivSubtype = { toFun := fun (a : Fin n) => ⟨↑a, ⋯⟩, invFun := fun (a : { i : ℕ // i < n }) => ⟨↑a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

coercions and constructions

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

@[deprecated Fin.ext_iff]

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

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

@[simp]

theorem Fin.mk_eq_mk {n a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} : ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

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 ⟨↑i, ⋯⟩

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

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 ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

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

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

Two elements of Fin k and Fin l are heq iff their values in ℕ coincide. This requires k = l. For the left implication without this assumption, see val_eq_val_of_heq.

order

theorem Fin.le_iff_val_le_val {n : ℕ} {a b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b

@[simp]

theorem Fin.val_fin_lt {n : ℕ} {a b : Fin n} : ↑a < ↑b ↔ a < b

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

@[simp]

theorem Fin.val_fin_le {n : ℕ} {a b : Fin n} : ↑a ≤ ↑b ↔ a ≤ b

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

theorem Fin.min_val {n : ℕ} {a : Fin n} : ↑a ⊓ n = ↑a

theorem Fin.max_val {n : ℕ} {a : Fin n} : ↑a ⊔ n = n

def Fin.valEmbedding {n : ℕ} : Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

• Fin.valEmbedding = { toFun := Fin.val, inj' := ⋯ }

@[simp]

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

@[simp]

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

instance Fin.instWellFoundedRelation_mathlib {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.instWellFoundedRelation_mathlib = measure Fin.val

@[deprecated Fin.ofNat']

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 = ⟨i % n, ⋯⟩

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

theorem Fin.cast_eq_self {n : ℕ} (a : Fin n) : Fin.cast ⋯ a = a

@[simp]

theorem Fin.cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l] (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0

theorem Fin.cast_injective {k l : ℕ} (h : k = l) : Function.Injective (Fin.cast h)

theorem Fin.rev_involutive {n : ℕ} : Function.Involutive Fin.rev

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 ⋯

@[simp]

theorem Fin.revPerm_symm_apply {n : ℕ} (i : Fin n) : (Equiv.symm Fin.revPerm) i = i.rev

@[simp]

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

theorem Fin.rev_injective {n : ℕ} : Function.Injective Fin.rev

theorem Fin.rev_surjective {n : ℕ} : Function.Surjective Fin.rev

theorem Fin.rev_bijective {n : ℕ} : Function.Bijective Fin.rev

@[simp]

theorem Fin.revPerm_symm {n : ℕ} : Equiv.symm Fin.revPerm = Fin.revPerm

theorem Fin.cast_rev {n m : ℕ} (i : Fin n) (h : n = m) : Fin.cast h i.rev = (Fin.cast h i).rev

theorem Fin.rev_eq_iff {n : ℕ} {i j : Fin n} : i.rev = j ↔ i = j.rev

theorem Fin.rev_ne_iff {n : ℕ} {i j : Fin n} : i.rev ≠ j ↔ i ≠ j.rev

theorem Fin.rev_lt_iff {n : ℕ} {i j : Fin n} : i.rev < j ↔ j.rev < i

theorem Fin.rev_le_iff {n : ℕ} {i j : Fin n} : i.rev ≤ j ↔ j.rev ≤ i

theorem Fin.lt_rev_iff {n : ℕ} {i j : Fin n} : i < j.rev ↔ j < i.rev

theorem Fin.le_rev_iff {n : ℕ} {i j : Fin n} : i ≤ j.rev ↔ j ≤ i.rev

@[simp]

theorem Fin.val_rev_zero {n : ℕ} [NeZero n] : ↑(Fin.rev 0) = n.pred

theorem Fin.last_pos' {n : ℕ} [NeZero n] : 0 < Fin.last n

theorem Fin.one_lt_last {n : ℕ} [NeZero n] : 1 < Fin.last (n + 1)

Coercions to ℤ and the fin_omega tactic.

theorem Fin.coe_int_sub_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

theorem Fin.coe_int_sub_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

theorem Fin.coe_int_add_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

theorem Fin.coe_int_add_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

def Fin.tacticFin_omega : Lean.ParserDescr

Preprocessor for omega to handle inequalities in Fin. Note that this involves a lot of case splitting, so may be slow.

Equations

• Fin.tacticFin_omega = Lean.ParserDescr.node `Fin.tacticFin_omega 1024 (Lean.ParserDescr.nonReservedSymbol "fin_omega" false)

addition, numerals, and coercion from Nat

@[simp]

theorem Fin.val_one' (n : ℕ) [NeZero n] : ↑1 = 1 % n

theorem Fin.val_one'' {n : ℕ} : ↑1 = 1 % (n + 1)

theorem Fin.nontrivial {n : ℕ} : Nontrivial (Fin (n + 2))

theorem Fin.nontrivial_iff_two_le {n : ℕ} : Nontrivial (Fin n) ↔ 2 ≤ n

instance Fin.inhabitedFinOneAdd (n : ℕ) : Inhabited (Fin (1 + n))

Equations

• Fin.inhabitedFinOneAdd n = inferInstance

@[simp]

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

instance Fin.instNatCast {n : ℕ} [NeZero n] : NatCast (Fin n)

Equations

• Fin.instNatCast = { natCast := fun (i : ℕ) => Fin.ofNat' n i }

theorem Fin.natCast_def {n : ℕ} [NeZero n] (a : ℕ) : ↑a = ⟨a % n, ⋯⟩

theorem Fin.val_add_eq_ite {n : ℕ} (a b : Fin n) : ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

theorem Fin.val_add_eq_of_add_lt {n : ℕ} {a b : Fin n} (huv : ↑a + ↑b < n) : ↑(a + b) = ↑a + ↑b

theorem Fin.intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) : ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

@[simp]

theorem Fin.ofNat'_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat' n a = ↑a

@[simp]

theorem Fin.val_natCast (a n : ℕ) [NeZero n] : ↑↑a = a % n

@[deprecated Fin.val_natCast]

theorem Fin.val_nat_cast (a n : ℕ) [NeZero n] : ↑↑a = a % n

Alias of Fin.val_natCast.

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.

@[simp]

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

If n is non-zero, converting the value of a Fin n to Fin n results in the same value.

@[simp]

theorem Fin.natCast_self (n : ℕ) [NeZero n] : ↑n = 0

@[deprecated Fin.natCast_self]

theorem Fin.nat_cast_self (n : ℕ) [NeZero n] : ↑n = 0

Alias of Fin.natCast_self.

@[simp]

theorem Fin.natCast_eq_zero {a n : ℕ} [NeZero n] : ↑a = 0 ↔ n ∣ a

@[deprecated Fin.natCast_eq_zero]

theorem Fin.nat_cast_eq_zero {a n : ℕ} [NeZero n] : ↑a = 0 ↔ n ∣ a

Alias of Fin.natCast_eq_zero.

@[simp]

theorem Fin.natCast_eq_last (n : ℕ) : ↑n = Fin.last n

@[deprecated Fin.natCast_eq_last]

theorem Fin.cast_nat_eq_last (n : ℕ) : ↑n = Fin.last n

Alias of Fin.natCast_eq_last.

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

theorem Fin.natCast_le_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a ≤ ↑b ↔ a ≤ b

theorem Fin.natCast_lt_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a < ↑b ↔ a < b

theorem Fin.natCast_mono {n a b : ℕ} (hbn : b ≤ n) (hab : a ≤ b) : ↑a ≤ ↑b

theorem Fin.natCast_strictMono {n a b : ℕ} (hbn : b ≤ n) (hab : a < b) : ↑a < ↑b

succ and casts into larger Fin types

theorem Fin.succ_injective (n : ℕ) : Function.Injective Fin.succ

def Fin.succEmb (n : ℕ) : Fin n ↪ Fin (n + 1)

Fin.succ as an Embedding

Equations

• Fin.succEmb n = { toFun := Fin.succ, inj' := ⋯ }

@[simp]

theorem Fin.val_succEmb {n : ℕ} : ⇑(Fin.succEmb n) = Fin.succ

@[simp]

theorem Fin.exists_succ_eq {n : ℕ} {x : Fin (n + 1)} : (∃ (y : Fin n), y.succ = x) ↔ x ≠ 0

theorem Fin.exists_succ_eq_of_ne_zero {n : ℕ} {x : Fin (n + 1)} (h : x ≠ 0) : ∃ (y : Fin n), y.succ = x

@[simp]

theorem Fin.succ_zero_eq_one' {n : ℕ} [NeZero n] : Fin.succ 0 = 1

theorem Fin.one_pos' {n : ℕ} [NeZero n] : 0 < 1

theorem Fin.zero_ne_one' {n : ℕ} [NeZero n] : 0 ≠ 1

@[simp]

theorem Fin.succ_one_eq_two' {n : ℕ} [NeZero n] : Fin.succ 1 = 2

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

@[simp]

theorem Fin.le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0

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

@[simp]

theorem Fin.castLE_inj {n m : ℕ} {hmn : m ≤ n} {a b : Fin m} : Fin.castLE hmn a = Fin.castLE hmn b ↔ a = b

@[simp]

theorem Fin.castAdd_inj {n m : ℕ} {a b : Fin m} : Fin.castAdd n a = Fin.castAdd n b ↔ a = b

theorem Fin.castLE_injective {n m : ℕ} (hmn : m ≤ n) : Function.Injective (Fin.castLE hmn)

theorem Fin.castAdd_injective (m n : ℕ) : Function.Injective (Fin.castAdd n)

theorem Fin.castSucc_injective (n : ℕ) : Function.Injective Fin.castSucc

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

Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

Equations

• Fin.castLEEmb h = { toFun := Fin.castLE h, inj' := ⋯ }

@[simp]

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

@[simp]

theorem Fin.coe_castLEEmb {m n : ℕ} (hmn : m ≤ n) : ⇑(Fin.castLEEmb hmn) = Fin.castLE hmn

theorem Fin.nonempty_embedding_iff {n m : ℕ} : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

theorem Fin.equiv_iff_eq {n m : ℕ} : Nonempty (Fin m ≃ Fin n) ↔ m = n

@[simp]

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

@[simp]

theorem Fin.castLE_comp_castSucc {n m : ℕ} (h : n + 1 ≤ m) : Fin.castLE h ∘ Fin.castSucc = Fin.castLE ⋯

@[simp]

theorem Fin.castLE_rfl (n : ℕ) : Fin.castLE ⋯ = id

@[simp]

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

@[simp]

theorem Fin.coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range (Fin.castLE h)) : ↑((Equiv.ofInjective (Fin.castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

theorem Fin.leftInverse_cast {n m : ℕ} (eq : n = m) : Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)

theorem Fin.rightInverse_cast {n m : ℕ} (eq : n = m) : Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)

theorem Fin.cast_lt_cast {n m : ℕ} (eq : n = m) {a b : Fin n} : Fin.cast eq a < Fin.cast eq b ↔ a < b

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

def finCongr {n m : ℕ} (eq : n = m) : Fin n ≃ Fin m

The 'identity' equivalence between Fin m and Fin n when m = n.

Equations

• finCongr eq = { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem finCongr_symm_apply {n m : ℕ} (eq : n = m) (i : Fin m) : (finCongr eq).symm i = Fin.cast ⋯ i

@[simp]

theorem finCongr_apply {n m : ℕ} (eq : n = m) (i : Fin n) : (finCongr eq) i = Fin.cast eq i

@[simp]

theorem finCongr_apply_mk {n m : ℕ} (h : m = n) (k : ℕ) (hk : k < m) : (finCongr h) ⟨k, hk⟩ = ⟨k, ⋯⟩

@[simp]

theorem finCongr_refl {n : ℕ} (h : n = n := ⋯) : finCongr h = Equiv.refl (Fin n)

@[simp]

theorem finCongr_symm {n m : ℕ} (h : m = n) : (finCongr h).symm = finCongr ⋯

@[simp]

theorem finCongr_apply_coe {n m : ℕ} (h : m = n) (k : Fin m) : ↑((finCongr h) k) = ↑k

theorem finCongr_symm_apply_coe {n m : ℕ} (h : m = n) (k : Fin n) : ↑((finCongr h).symm k) = ↑k

theorem finCongr_eq_equivCast {n m : ℕ} (h : n = m) : finCongr h = Equiv.cast ⋯

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

@[simp]

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

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

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

def Fin.castAddEmb {n : ℕ} (m : ℕ) : Fin n ↪ Fin (n + m)

Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

Equations

• Fin.castAddEmb m = Fin.castLEEmb ⋯

@[simp]

theorem Fin.castAddEmb_apply {n : ℕ} (m : ℕ) (i : Fin n) : (Fin.castAddEmb m) i = Fin.castLE ⋯ i

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

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

Equations

• Fin.castSuccEmb = Fin.castAddEmb 1

@[simp]

theorem Fin.castSuccEmb_apply {n : ℕ} (i : Fin n) : Fin.castSuccEmb i = Fin.castLE ⋯ i

@[simp]

theorem Fin.coe_castSuccEmb {n : ℕ} : ⇑Fin.castSuccEmb = Fin.castSucc

theorem Fin.castSucc_le_succ {n : ℕ} (i : Fin n) : i.castSucc ≤ i.succ

@[simp]

theorem Fin.castSucc_le_castSucc_iff {n : ℕ} {a b : Fin n} : a.castSucc ≤ b.castSucc ↔ a ≤ b

@[simp]

theorem Fin.succ_le_castSucc_iff {n : ℕ} {a b : Fin n} : a.succ ≤ b.castSucc ↔ a < b

@[simp]

theorem Fin.castSucc_lt_succ_iff {n : ℕ} {a b : Fin n} : a.castSucc < b.succ ↔ a ≤ b

theorem Fin.le_of_castSucc_lt_of_succ_lt {n : ℕ} {a b : Fin (n + 1)} {i : Fin n} (hl : i.castSucc < a) (hu : b < i.succ) : b < a

theorem Fin.castSucc_lt_or_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p < i.succ

@[deprecated Fin.castSucc_lt_or_lt_succ]

theorem Fin.succAbove_lt_gt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p < i.succ

Alias of Fin.castSucc_lt_or_lt_succ.

theorem Fin.succ_le_or_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.succ ≤ p ∨ p ≤ i.castSucc

theorem Fin.exists_castSucc_eq_of_ne_last {n : ℕ} {x : Fin (n + 1)} (h : x ≠ Fin.last n) : ∃ (y : Fin n), y.castSucc = x

theorem Fin.forall_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (Fin.last n)

theorem Fin.eq_castSucc_or_eq_last {n : ℕ} (i : Fin (n + 1)) : (∃ (j : Fin n), i = j.castSucc) ∨ i = Fin.last n

theorem Fin.exists_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ (i : Fin (n + 1)), P i) ↔ (∃ (i : Fin n), P i.castSucc) ∨ P (Fin.last n)

@[simp]

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

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

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

castSucc i is positive when i is positive.

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

@[simp]

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

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

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

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

theorem Fin.castSucc_ne_zero_of_lt {n : ℕ} {p i : Fin n} (h : p < i) : i.castSucc ≠ 0

theorem Fin.succ_ne_last_iff {n : ℕ} (a : Fin (n + 1)) : a.succ ≠ Fin.last (n + 1) ↔ a ≠ Fin.last n

theorem Fin.succ_ne_last_of_lt {n : ℕ} {p i : Fin n} (h : i < p) : i.succ ≠ Fin.last n

@[simp]

theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} : ↑↑a = a.castSucc

theorem Fin.coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} : ↑↑j < ↑↑k ↔ j < k

@[simp]

theorem Fin.range_castSucc {n : ℕ} : Set.range Fin.castSucc = {i : Fin n.succ | ↑i < n}

@[simp]

theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin n.succ) (hi : i ∈ Set.range Fin.castSucc) : ↑((Equiv.ofInjective Fin.castSucc ⋯).symm ⟨i, hi⟩) = ↑i

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

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

Equations

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

@[simp]

theorem Fin.addNatEmb_apply {n : ℕ} (m : ℕ) (x✝ : Fin n) : (Fin.addNatEmb m) x✝ = x✝.addNat m

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

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

Equations

• Fin.natAddEmb n = { toFun := Fin.natAdd n, inj' := ⋯ }

@[simp]

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

pred

theorem Fin.pred_one' {n : ℕ} [NeZero n] (h : 1 ≠ 0 := ⋯) : Fin.pred 1 h = 0

theorem Fin.pred_last {n : ℕ} (h : ¬Fin.last (n + 1) = 0 := ⋯) : (Fin.last (n + 1)).pred h = Fin.last n

theorem Fin.pred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : i.pred hi < j ↔ i < j.succ

theorem Fin.lt_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j < i.pred hi ↔ j.succ < i

theorem Fin.pred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : i.pred hi ≤ j ↔ i ≤ j.succ

theorem Fin.le_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j ≤ i.pred hi ↔ j.succ ≤ i

theorem Fin.castSucc_pred_eq_pred_castSucc {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) (ha' : a.castSucc ≠ 0 := ⋯) : (a.pred ha).castSucc = a.castSucc.pred ha'

theorem Fin.castSucc_pred_add_one_eq {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc + 1 = a

theorem Fin.le_pred_castSucc_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) : b ≤ a.castSucc.pred ha ↔ b < a

theorem Fin.pred_castSucc_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) : a.castSucc.pred ha < b ↔ a ≤ b

theorem Fin.pred_castSucc_lt {n : ℕ} {a : Fin (n + 1)} (ha : a.castSucc ≠ 0) : a.castSucc.pred ha < a

theorem Fin.le_castSucc_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) : b ≤ (a.pred ha).castSucc ↔ b < a

theorem Fin.castSucc_pred_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc < b ↔ a ≤ b

theorem Fin.castSucc_pred_lt {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc < a

@[inline]

def Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : Fin n

castPred i sends i : Fin (n + 1) to Fin n as long as i ≠ last n.

Equations

• i.castPred h = i.castLT ⋯

@[simp]

theorem Fin.castLT_eq_castPred {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) (h' : ¬i = Fin.last n := ⋯) : i.castLT h = i.castPred h'

@[simp]

theorem Fin.coe_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : ↑(i.castPred h) = ↑i

@[simp]

theorem Fin.castPred_castSucc {n : ℕ} {i : Fin n} (h' : ¬i.castSucc = Fin.last n := ⋯) : i.castSucc.castPred h' = i

@[simp]

theorem Fin.castSucc_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : (i.castPred h).castSucc = i

theorem Fin.castPred_eq_iff_eq_castSucc {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (j : Fin n) : i.castPred hi = j ↔ i = j.castSucc

@[simp]

theorem Fin.castPred_mk {n : ℕ} (i : ℕ) (h₁ : i < n) (h₂ : i < n.succ := ⋯) (h₃ : ⟨i, h₂⟩ ≠ Fin.last n := ⋯) : ⟨i, h₂⟩.castPred h₃ = ⟨i, h₁⟩

theorem Fin.castPred_le_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : i.castPred hi ≤ j.castPred hj ↔ i ≤ j

theorem Fin.castPred_lt_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : i.castPred hi < j.castPred hj ↔ i < j

theorem Fin.castPred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : i.castPred hi < j ↔ i < j.castSucc

theorem Fin.lt_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : j < i.castPred hi ↔ j.castSucc < i

theorem Fin.castPred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : i.castPred hi ≤ j ↔ i ≤ j.castSucc

theorem Fin.le_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : j ≤ i.castPred hi ↔ j.castSucc ≤ i

theorem Fin.castPred_inj {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : i.castPred hi = j.castPred hj ↔ i = j

theorem Fin.castPred_zero' {n : ℕ} [NeZero n] (h : ¬0 = Fin.last n := ⋯) : Fin.castPred 0 h = 0

theorem Fin.castPred_zero {n : ℕ} (h : ¬0 = Fin.last (n + 1) := ⋯) : Fin.castPred 0 h = 0

@[simp]

theorem Fin.castPred_one {n : ℕ} [NeZero n] (h : ¬1 = Fin.last (n + 1) := ⋯) : Fin.castPred 1 h = 1

theorem Fin.rev_pred {n : ℕ} {i : Fin (n + 1)} (h : i ≠ 0) (h' : i.rev ≠ Fin.last n := ⋯) : (i.pred h).rev = i.rev.castPred h'

theorem Fin.rev_castPred {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) (h' : i.rev ≠ 0 := ⋯) : (i.castPred h).rev = i.rev.pred h'

theorem Fin.succ_castPred_eq_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) (ha' : a.succ ≠ Fin.last (n + 1) := ⋯) : (a.castPred ha).succ = a.succ.castPred ha'

theorem Fin.succ_castPred_eq_add_one {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) : (a.castPred ha).succ = a + 1

theorem Fin.castpred_succ_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)) : a.succ.castPred ha ≤ b ↔ a < b

theorem Fin.lt_castPred_succ_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)) : b < a.succ.castPred ha ↔ b ≤ a

theorem Fin.lt_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)) : a < a.succ.castPred ha

theorem Fin.succ_castPred_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) : (a.castPred ha).succ ≤ b ↔ a < b

theorem Fin.lt_succ_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) : b < (a.castPred ha).succ ↔ b ≤ a

theorem Fin.lt_succ_castPred {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) : a < (a.castPred ha).succ

theorem Fin.castPred_le_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) (hb : b ≠ 0) : a.castPred ha ≤ b.pred hb ↔ a < b

theorem Fin.pred_lt_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ Fin.last n) : a.pred ha < b.castPred hb ↔ a ≤ b

theorem Fin.pred_lt_castPred {n : ℕ} {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ Fin.last n) : a.pred h₁ < a.castPred h₂

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

• p.succAbove i = if i.castSucc < p then i.castSucc else i.succ

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

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.

theorem Fin.succAbove_of_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.succ ≤ p) : p.succAbove i = i.castSucc

theorem Fin.succAbove_of_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ i.castSucc) : p.succAbove i = i.succ

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.

theorem Fin.succAbove_of_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) : p.succAbove i = i.succ

theorem Fin.succAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : p < i) : p.succ.succAbove i = i.succ

theorem Fin.succAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) : p.succ.succAbove i = i.castSucc

@[simp]

theorem Fin.succAbove_succ_self {n : ℕ} (j : Fin n) : j.succ.succAbove j = j.castSucc

theorem Fin.succAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : i < p) : p.castSucc.succAbove i = i.castSucc

theorem Fin.succAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) : p.castSucc.succAbove i = i.succ

@[simp]

theorem Fin.succAbove_castSucc_self {n : ℕ} (j : Fin n) : j.castSucc.succAbove j = j.succ

theorem Fin.succAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) (hi : i ≠ 0 := ⋯) : p.succAbove (i.pred hi) = i

theorem Fin.succAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) : p.succAbove (i.pred hi) = (i.pred hi).castSucc

@[simp]

theorem Fin.succAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0) : p.succAbove (p.pred h) = (p.pred h).castSucc

theorem Fin.succAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) (hi : i ≠ Fin.last n := ⋯) : p.succAbove (i.castPred hi) = i

theorem Fin.succAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ Fin.last n) : p.succAbove (i.castPred hi) = (i.castPred hi).succ

theorem Fin.succAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ Fin.last n) : p.succAbove (p.castPred h) = (p.castPred h).succ

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

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

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

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

theorem Fin.ne_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p ≠ p.succAbove i

theorem Fin.succAbove_right_injective {n : ℕ} {p : Fin (n + 1)} : Function.Injective p.succAbove

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

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

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

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

Fin.succAbove p as an Embedding.

Equations

• p.succAboveEmb = { toFun := p.succAbove, inj' := ⋯ }

@[simp]

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

@[simp]

theorem Fin.coe_succAboveEmb {n : ℕ} (p : Fin (n + 1)) : ⇑p.succAboveEmb = p.succAbove

@[simp]

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

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

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

@[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.

theorem Fin.succAbove_zero_apply {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ

@[simp]

theorem Fin.succAbove_ne_last_last {n : ℕ} {a : Fin (n + 2)} (h : a ≠ Fin.last (n + 1)) : a.succAbove (Fin.last n) = Fin.last (n + 1)

theorem Fin.succAbove_eq_last_iff {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) : a.succAbove b = Fin.last (n + 1) ↔ b = Fin.last n

theorem Fin.succAbove_ne_last {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) : a.succAbove b ≠ Fin.last (n + 1)

@[simp]

theorem Fin.succAbove_last {n : ℕ} : (Fin.last n).succAbove = Fin.castSucc

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

theorem Fin.succAbove_last_apply {n : ℕ} (i : Fin n) : (Fin.last n).succAbove i = i.castSucc

@[deprecated]

theorem Fin.succAbove_lt_ge {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p ≤ i.castSucc

theorem Fin.succAbove_lt_iff_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.castSucc < 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.

theorem Fin.succAbove_lt_iff_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.succ ≤ p

theorem Fin.lt_succAbove_iff_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p ≤ i.castSucc

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

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

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

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

theorem Fin.castPred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : y.succAbove x ≠ Fin.last n := ⋯) : (y.succAbove x).castPred h' = x

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

theorem Fin.exists_succAbove_eq {n : ℕ} {x y : Fin (n + 1)} (h : x ≠ y) : ∃ (z : Fin n), y.succAbove z = x

@[simp]

theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x y : Fin (n + 1)} : (∃ (z : Fin n), x.succAbove z = y) ↔ y ≠ x

@[simp]

theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) : Set.range p.succAbove = {p}ᶜ

The range of p.succAbove is everything except p.

@[simp]

theorem Fin.range_succ (n : ℕ) : Set.range Fin.succ = {0}ᶜ

theorem Fin.succAbove_left_injective {n : ℕ} : Function.Injective Fin.succAbove

succAbove is injective at the pivot

@[simp]

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

succAbove is injective at the pivot

@[simp]

theorem Fin.zero_succAbove {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ

@[simp]

theorem Fin.succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) : i.succ.succAbove 0 = 0

@[simp]

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

succ commutes with succAbove.

@[simp]

theorem Fin.castSucc_succAbove_castSucc {n : ℕ} {i : Fin (n + 1)} {j : Fin n} : i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

castSucc commutes with succAbove.

theorem Fin.pred_succAbove_pred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : a.succAbove b ≠ 0 := ⋯) : (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

pred commutes with succAbove.

theorem Fin.castPred_succAbove_castPred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) (hk : a.succAbove b ≠ Fin.last (n + 1) := ⋯) : (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

castPred commutes with succAbove.

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

rev commutes with succAbove.

theorem Fin.one_succAbove_zero {n : ℕ} : Fin.succAbove 1 0 = 0

@[simp]

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

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

@[simp]

theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) : Fin.succAbove 1 j.succ = j.succ.succ

@[simp]

theorem Fin.one_succAbove_one {n : ℕ} : Fin.succAbove 1 1 = 2

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

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

Equations

• p.predAbove i = if h : p.castSucc < i then i.pred ⋯ else i.castPred ⋯

theorem Fin.predAbove_of_le_castSucc {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc) (hi : i ≠ Fin.last n := ⋯) : p.predAbove i = i.castPred hi

theorem Fin.predAbove_of_lt_succ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : i ≠ Fin.last n := ⋯) : p.predAbove i = i.castPred hi

theorem Fin.predAbove_of_castSucc_lt {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : i ≠ 0 := ⋯) : p.predAbove i = i.pred hi

theorem Fin.predAbove_of_succ_le {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i) (hi : i ≠ 0 := ⋯) : p.predAbove i = i.pred hi

theorem Fin.predAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : i < p) (hi : i.succ ≠ Fin.last n := ⋯) : p.predAbove i.succ = i.succ.castPred hi

theorem Fin.predAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) : p.predAbove i.succ = i

@[simp]

theorem Fin.predAbove_succ_self {n : ℕ} (p : Fin n) : p.predAbove p.succ = p

theorem Fin.predAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : p < i) (hi : i.castSucc ≠ 0 := ⋯) : p.predAbove i.castSucc = i.castSucc.pred hi

theorem Fin.predAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) : p.predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_castSucc_self {n : ℕ} (p : Fin n) : p.predAbove p.castSucc = p

theorem Fin.predAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) (hp : p ≠ 0 := ⋯) (hi : i ≠ Fin.last n := ⋯) : (p.pred hp).predAbove i = i.castPred hi

theorem Fin.predAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0) (hi : i ≠ 0 := ⋯) : (p.pred hp).predAbove i = i.pred hi

theorem Fin.predAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0) : (p.pred hp).predAbove p = p.pred hp

theorem Fin.predAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) (hp : p ≠ Fin.last n := ⋯) (hi : i ≠ 0 := ⋯) : (p.castPred hp).predAbove i = i.pred hi

theorem Fin.predAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ Fin.last n) (hi : i ≠ Fin.last n := ⋯) : (p.castPred hp).predAbove i = i.castPred hi

theorem Fin.predAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ Fin.last n) : (p.castPred hp).predAbove p = p.castPred hp

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

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

@[simp]

theorem Fin.predAbove_right_zero {n : ℕ} [NeZero n] {i : Fin n} : i.predAbove 0 = 0

@[simp]

theorem Fin.predAbove_zero_succ {n : ℕ} [NeZero n] {i : Fin n} : Fin.predAbove 0 i.succ = i

@[simp]

theorem Fin.succ_predAbove_zero {n : ℕ} [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) : (Fin.predAbove 0 j).succ = j

@[simp]

theorem Fin.predAbove_zero_of_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) : Fin.predAbove 0 i = i.pred hi

theorem Fin.predAbove_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} : Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

@[simp]

theorem Fin.predAbove_right_last {n : ℕ} {i : Fin (n + 1)} : i.predAbove (Fin.last (n + 1)) = Fin.last n

@[simp]

theorem Fin.predAbove_last_castSucc {n : ℕ} {i : Fin (n + 1)} : (Fin.last n).predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_last_of_ne_last {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ Fin.last (n + 1)) : (Fin.last n).predAbove i = i.castPred hi

theorem Fin.predAbove_last_apply {n : ℕ} {i : Fin (n + 2)} : (Fin.last n).predAbove i = if hi : i = Fin.last (n + 1) then Fin.last n else i.castPred hi

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.castSucc) : p.castSucc.succAbove (p.predAbove 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.

@[simp]

theorem Fin.predAbove_succAbove {n : ℕ} (p i : Fin n) : p.predAbove (p.castSucc.succAbove i) = i

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

@[simp]

theorem Fin.succ_predAbove_succ {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.succ.predAbove b.succ = (a.predAbove b).succ

succ commutes with predAbove.

@[simp]

theorem Fin.castSucc_predAbove_castSucc {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

castSucc commutes with predAbove.

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

rev commutes with predAbove.

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

• i.divNat = ⟨↑i / n, ⋯⟩

@[simp]

theorem Fin.coe_divNat {n m : ℕ} (i : Fin (m * n)) : ↑i.divNat = ↑i / n

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

• i.modNat = ⟨↑i % n, ⋯⟩

@[simp]

theorem Fin.coe_modNat {n m : ℕ} (i : Fin (m * n)) : ↑i.modNat = ↑i % n

theorem Fin.modNat_rev {n m : ℕ} (i : Fin (m * n)) : i.rev.modNat = i.modNat.rev

recursion and induction principles

theorem Fin.liftFun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} : ((fun (x1 x2 : Fin (n + 1)) => x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

instance Fin.neg (n : ℕ) : Neg (Fin n)

Negation on Fin n

Equations

• Fin.neg n = { neg := fun (a : Fin n) => ⟨(n - ↑a) % n, ⋯⟩ }

theorem Fin.neg_def {n : ℕ} (a : Fin n) : -a = ⟨(n - ↑a) % n, ⋯⟩

theorem Fin.coe_neg {n : ℕ} (a : Fin n) : ↑(-a) = (n - ↑a) % n

theorem Fin.eq_zero (n : Fin 1) : n = 0

@[deprecated Fin.val_eq_zero]

theorem Fin.coe_fin_one (a : Fin 1) : ↑a = 0

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

@[simp]

theorem Fin.coe_neg_one {n : ℕ} : ↑(-1) = n

theorem Fin.last_sub {n : ℕ} (i : Fin (n + 1)) : Fin.last n - i = i.rev

theorem Fin.add_one_le_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : a + 1 ≤ b

theorem Fin.exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ k ≤ b, b = a + k

theorem Fin.exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

theorem Fin.pos_of_ne_zero {n : ℕ} {a : Fin (n + 1)} (h : a ≠ 0) : 0 < a

theorem Fin.sub_succ_le_sub_of_le {n : ℕ} {u v : Fin (n + 2)} (h : u < v) : v - (u + 1) < v - u

@[simp]

theorem Fin.coe_natCast_eq_mod (m n : ℕ) [NeZero m] : ↑↑n = n % m

theorem Fin.coe_ofNat_eq_mod (m n : ℕ) [NeZero m] : ↑(OfNat.ofNat n) = OfNat.ofNat n % m

mul

theorem Fin.mul_one' {n : ℕ} [NeZero n] (k : Fin n) : k * 1 = k

theorem Fin.one_mul' {n : ℕ} [NeZero n] (k : Fin n) : 1 * k = k

theorem Fin.mul_zero' {n : ℕ} [NeZero n] (k : Fin n) : k * 0 = 0

theorem Fin.zero_mul' {n : ℕ} [NeZero n] (k : Fin n) : 0 * k = 0