mathlib documentation

data.fin

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 #

Casts #

Operation on tuples #

We interpret maps Π i : fin n, α i as tuples (α 0, …, α (n-1)). If α i is a constant map, then tuples are isomorphic (but not definitionally equal) to vectors.

We define the following operations:

Misc definitions #

source
def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) :
α x

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

Equations
source
@[instance]
theorem fact.succ.pos {n : ℕ} :
fact (0 < n.succ)
source
@[instance]
theorem fact.bit0.pos {n : ℕ} [h : fact (0 < n)] :
fact (0 < bit0 n)
source
@[instance]
theorem fact.bit1.pos {n : ℕ} :
fact (0 < bit1 n)
source
@[instance]
theorem fact.pow.pos {p n : ℕ} [h : fact (0 < p)] :
fact (0 < p ^ n)
source
@[protected, instance]
def fin.fin_to_nat (n : ℕ) :
has_coe (fin n) ℕ
Equations

coercions and constructions #

source
@[protected, simp]
theorem fin.eta {n : ℕ} (a : fin n) (h : ↑a < n) :
⟨↑a, h⟩ = a
source
@[ext]
theorem fin.ext {n : ℕ} {a b : fin n} (h : ↑a = ↑b) :
a = b
source
theorem fin.ext_iff {n : ℕ} (a b : fin n) :
a = b ↔ ↑a = ↑b
source
theorem fin.coe_injective {n : ℕ} :
function.injective coe
source
theorem fin.eq_iff_veq {n : ℕ} (a b : fin n) :
a = b ↔ a.val = b.val
source
theorem fin.ne_iff_vne {n : ℕ} (a b : fin n) :
a ≠ b ↔ a.val ≠ b.val
source
@[simp]
theorem fin.mk_eq_subtype_mk {n : ℕ} (a : ℕ) (h : a < n) :
fin.mk a h = ⟨a, h⟩
source
@[protected]
theorem fin.mk.inj_iff {n a b : ℕ} {ha : a < n} {hb : b < n} :
⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b
source
theorem fin.mk_val {m n : ℕ} (h : m < n) :
⟨m, h⟩.val = m
source
theorem fin.eq_mk_iff_coe_eq {n : ℕ} {a : fin n} {k : ℕ} {hk : k < n} :
a = ⟨k, hk⟩ ↔ ↑a = k
source
@[simp, norm_cast]
theorem fin.coe_mk {m n : ℕ} (h : m < n) :
↑⟨m, h⟩ = m
source
theorem fin.mk_coe {n : ℕ} (i : fin n) :
⟨↑i, _⟩ = i
source
theorem fin.coe_eq_val {n : ℕ} (a : fin n) :
↑a = a.val
source
@[simp]
theorem fin.val_eq_coe {n : ℕ} (a : fin n) :
a.val = ↑a
source
@[protected]
theorem fin.heq_fun_iff {α : Sort u_1} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :
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).

source
@[protected]
theorem fin.heq_ext_iff {k l : ℕ} (h : k = l) {i : fin k} {j : fin l} :
i == j ↔ ↑i = ↑j
source
theorem fin.exists_iff {n : ℕ} {p : fin n → Prop} :
(∃ (i : fin n), p i) ↔ ∃ (i : ℕ) (h : i < n), p ⟨i, h⟩
source
theorem fin.forall_iff {n : ℕ} {p : fin n → Prop} :
(∀ (i : fin n), p i) ↔ ∀ (i : ℕ) (h : i < n), p ⟨i, h⟩

order #

source
theorem fin.is_lt {n : ℕ} (i : fin n) :
↑i < n
source
theorem fin.is_le {n : ℕ} (i : fin (n + 1)) :
↑i ≤ n
source
theorem fin.lt_iff_coe_lt_coe {n : ℕ} {a b : fin n} :
a < b ↔ ↑a < ↑b
source
theorem fin.le_iff_coe_le_coe {n : ℕ} {a b : fin n} :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem fin.mk_lt_of_lt_coe {n : ℕ} {b : fin n} {a : ℕ} (h : a < ↑b) :
⟨a, _⟩ < b
source
theorem fin.mk_le_of_le_coe {n : ℕ} {b : fin n} {a : ℕ} (h : a ≤ ↑b) :
⟨a, _⟩ ≤ b
source
@[simp, norm_cast]
theorem fin.coe_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.

source
@[simp, norm_cast]
theorem fin.coe_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.

source
@[protected, instance]
def fin.linear_order {n : ℕ} :
linear_order (fin n)
Equations
source
def fin.coe_embedding (n : ℕ) :
fin n ↪o ℕ

The inclusion map fin n → ℕ is a relation embedding.

Equations
source
@[protected, instance]
def fin.fin.lt.is_well_order (n : ℕ) :
is_well_order (fin n) has_lt.lt

The ordering on fin n is a well order.

source
@[protected, instance]
def fin.has_well_founded {n : ℕ} :
has_well_founded (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 has_well_founded instance:

def factorial {n : ℕ} : fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
Equations
source
@[simp]
theorem fin.coe_zero {n : ℕ} :
↑0 = 0
source
@[simp]
theorem fin.val_zero' (n : ℕ) :
0.val = 0
source
@[simp]
theorem fin.mk_zero {n : ℕ} :
⟨0, _⟩ = 0
source
theorem fin.zero_le {n : ℕ} (a : fin (n + 1)) :
0 ≤ a
source
theorem fin.pos_iff_ne_zero {n : ℕ} (a : fin (n + 1)) :
0 < a ↔ a ≠ 0
source
def fin.last (n : ℕ) :
fin (n + 1)

The greatest value of fin (n+1)

Equations
source
@[simp, norm_cast]
theorem fin.coe_last (n : ℕ) :
↑(fin.last n) = n
source
theorem fin.last_val (n : ℕ) :
(fin.last n).val = n
source
theorem fin.le_last {n : ℕ} (i : fin (n + 1)) :
i ≤ fin.last n
source
@[protected, instance]
def fin.bounded_lattice {n : ℕ} :
bounded_lattice (fin (n + 1))
Equations
source
theorem fin.last_pos {n : ℕ} :
0 < fin.last (n + 1)
source
theorem fin.eq_last_of_not_lt {n : ℕ} {i : fin (n + 1)} (h : ¬↑i < n) :
i = fin.last n
source
@[simp]
theorem fin.coe_order_iso_apply {n m : ℕ} (e : fin n ≃o fin m) (i : fin n) :
↑(⇑e i) = ↑i

If e is an order_iso 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
@[protected, instance]
def fin.order_iso_subsingleton {n : ℕ} {α : Type u_1} [preorder α] :
subsingleton (fin n ≃o α)
source
@[protected, instance]
def fin.order_iso_subsingleton' {n : ℕ} {α : Type u_1} [preorder α] :
subsingleton (α ≃o fin n)
source
@[protected, instance]
def fin.order_iso_unique {n : ℕ} :
unique (fin n ≃o fin n)
Equations
source
theorem fin.strict_mono_unique {n : ℕ} {α : Type u_1} [preorder α] {f g : fin n → α} (hf : strict_mono f) (hg : strict_mono 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.order_embedding_eq {n : ℕ} {α : Type u_1} [preorder α] {f g : fin n ↪o α} (h : set.range ⇑f = set.range ⇑g) :
f = g

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

source
theorem fin.strict_mono_iff_lt_succ {n : ℕ} {α : Type u_1} [preorder α] {f : fin n → α} :
strict_mono f ↔ ∀ (i : ℕ) (h : i + 1 < n), f ⟨i, _⟩ < f ⟨i + 1, h⟩

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

addition, numerals, and coercion from nat #

source
def fin.of_nat' {n : ℕ} [h : fact (0 < n)] (i : ℕ) :
fin n

convert a ℕ to fin n, provided n is positive

Equations
source
theorem fin.one_val {n : ℕ} :
1.val = 1 % (n + 1)
source
theorem fin.coe_one' {n : ℕ} :
↑1 = 1 % (n + 1)
source
@[simp]
theorem fin.val_one {n : ℕ} :
1.val = 1
source
@[simp]
theorem fin.coe_one {n : ℕ} :
↑1 = 1
source
@[simp]
theorem fin.mk_one {n : ℕ} :
⟨1, _⟩ = 1
source
@[protected, instance]
def fin.nontrivial {n : ℕ} :
nontrivial (fin (n + 2))
source
@[protected, simp]
theorem fin.add_zero {n : ℕ} (k : fin (n + 1)) :
k + 0 = k
source
@[protected, simp]
theorem fin.zero_add {n : ℕ} (k : fin (n + 1)) :
0 + k = k
source
@[protected, instance]
def fin.add_comm_monoid (n : ℕ) :
add_comm_monoid (fin (n + 1))
Equations
source
theorem fin.val_add {n : ℕ} (a b : fin n) :
(a + b).val = (a.val + b.val) % n
source
theorem fin.coe_add {n : ℕ} (a b : fin n) :
↑(a + b) = (↑a + ↑b) % n
source
theorem fin.coe_bit0 {n : ℕ} (k : fin n) :
↑(bit0 k) = bit0 ↑k % n
source
theorem fin.coe_bit1 {n : ℕ} (k : fin (n + 1)) :
↑(bit1 k) = bit1 ↑k % (n + 1)
source
theorem fin.coe_add_one_of_lt {n : ℕ} {i : fin n.succ} (h : i < fin.last n) :
↑(i + 1) = ↑i + 1
source
@[simp]
theorem fin.last_add_one (n : ℕ) :
fin.last n + 1 = 0
source
theorem fin.coe_add_one {n : ℕ} (i : fin (n + 1)) :
↑(i + 1) = ite (i = fin.last n) 0 (↑i + 1)
source
@[simp]
theorem fin.mk_bit0 {m n : ℕ} (h : bit0 m < n) :
⟨bit0 m, h⟩ = bit0 ⟨m, _⟩
source
@[simp]
theorem fin.mk_bit1 {m n : ℕ} (h : bit1 m < n + 1) :
⟨bit1 m, h⟩ = bit1 ⟨m, _⟩
source
@[simp]
theorem fin.val_two {n : ℕ} :
2.val = 2
source
@[simp]
theorem fin.coe_two {n : ℕ} :
↑2 = 2
source
@[simp]
theorem fin.of_nat_eq_coe (n a : ℕ) :
fin.of_nat a = ↑a
source
theorem fin.coe_val_of_lt {n a : ℕ} (h : a < n + 1) :
↑a.val = a

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

source
theorem fin.coe_val_eq_self {n : ℕ} (a : fin (n + 1)) :
↑(a.val) = a

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

source
theorem fin.coe_coe_of_lt {n a : ℕ} (h : a < n + 1) :
↑↑a = a

Coercing an in-range number to fin (n + 1), and converting back to ℕ, results in that number.

source
@[simp]
theorem fin.coe_coe_eq_self {n : ℕ} (a : fin (n + 1)) :
↑↑a = a

Converting a fin (n + 1) to ℕ and back results in the same value.

source
theorem fin.coe_nat_eq_last (n : ℕ) :
↑n = fin.last n
source
theorem fin.le_coe_last {n : ℕ} (i : fin (n + 1)) :
i ≤ ↑n
source
theorem fin.add_one_pos {n : ℕ} (i : fin (n + 1)) (h : i < fin.last n) :
0 < i + 1
source
theorem fin.one_pos {n : ℕ} :
0 < 1
source
theorem fin.zero_ne_one {n : ℕ} :
0 ≠ 1
source
@[simp]
theorem fin.zero_eq_one_iff {n : ℕ} :
0 = 1 ↔ n = 0
source
@[simp]
theorem fin.one_eq_zero_iff {n : ℕ} :
1 = 0 ↔ n = 0

succ and casts into larger fin types #

source
@[simp]
theorem fin.coe_succ {n : ℕ} (j : fin n) :
↑(j.succ) = ↑j + 1
source
theorem fin.succ_pos {n : ℕ} (a : fin n) :
0 < a.succ
source
def fin.succ_embedding (n : ℕ) :
fin n ↪o fin (n + 1)

fin.succ as an order_embedding

Equations
source
@[simp]
theorem fin.coe_succ_embedding {n : ℕ} :
⇑(fin.succ_embedding n) = fin.succ
source
@[simp]
theorem fin.succ_le_succ_iff {n : ℕ} {a b : fin n} :
a.succ ≤ b.succ ↔ a ≤ b
source
@[simp]
theorem fin.succ_lt_succ_iff {n : ℕ} {a b : fin n} :
a.succ < b.succ ↔ a < b
source
theorem fin.succ_injective (n : ℕ) :
function.injective fin.succ
source
@[simp]
theorem fin.succ_inj {n : ℕ} {a b : fin n} :
a.succ = b.succ ↔ a = b
source
theorem fin.succ_ne_zero {n : ℕ} (k : fin n) :
k.succ ≠ 0
source
@[simp]
theorem fin.succ_zero_eq_one {n : ℕ} :
0.succ = 1
source
@[simp]
theorem fin.succ_one_eq_two {n : ℕ} :
1.succ = 2
source
@[simp]
theorem fin.succ_mk (n i : ℕ) (h : i < n) :
fin.succ ⟨i, h⟩ = ⟨i + 1, _⟩
source
theorem fin.mk_succ_pos {n : ℕ} (i : ℕ) (h : i < n) :
0 < ⟨i.succ, _⟩
source
theorem fin.one_lt_succ_succ {n : ℕ} (a : fin n) :
1 < a.succ.succ
source
theorem fin.succ_succ_ne_one {n : ℕ} (a : fin n) :
a.succ.succ ≠ 1
source
def fin.cast_lt {n m : ℕ} (i : fin m) (h : i.val < n) :
fin n

cast_lt i h embeds i into a fin where h proves it belongs into.

Equations
source
@[simp]
theorem fin.coe_cast_lt {n m : ℕ} (i : fin m) (h : i.val < n) :
↑(i.cast_lt h) = ↑i
source
@[simp]
theorem fin.cast_lt_mk (i n m : ℕ) (hn : i < n) (hm : i < m) :
fin.cast_lt ⟨i, hn⟩ hm = ⟨i, hm⟩
source
def fin.cast_le {n m : ℕ} (h : n ≤ m) :
fin n ↪o fin m

cast_le h i embeds i into a larger fin type.

Equations
source
@[simp]
theorem fin.coe_cast_le {n m : ℕ} (h : n ≤ m) (i : fin n) :
↑(⇑(fin.cast_le h) i) = ↑i
source
@[simp]
theorem fin.cast_le_mk (i n m : ℕ) (hn : i < n) (h : n ≤ m) :
⇑(fin.cast_le h) ⟨i, hn⟩ = ⟨i, _⟩
source
@[simp]
theorem fin.cast_le_zero {n m : ℕ} (h : n.succ ≤ m.succ) :
⇑(fin.cast_le h) 0 = 0
source
@[simp]
theorem fin.range_cast_le {n k : ℕ} (h : n ≤ k) :
set.range ⇑(fin.cast_le h) = {i : fin k | ↑i < n}
source
@[simp]
theorem fin.coe_of_injective_cast_le_symm {n k : ℕ} (h : n ≤ k) (i : fin k) (hi : i ∈ set.range ⇑(fin.cast_le h)) :
↑(⇑((equiv.of_injective ⇑(fin.cast_le h) _).symm) ⟨i, hi⟩) = ↑i
source
def fin.cast {n m : ℕ} (eq : n = m) :
fin n ≃o fin m

cast eq i embeds i into a equal fin type.

Equations
source
@[simp]
theorem fin.symm_cast {n m : ℕ} (h : n = m) :
(fin.cast h).symm = fin.cast _
source
theorem fin.coe_cast {n m : ℕ} (h : n = m) (i : fin n) :
↑(⇑(fin.cast h) i) = ↑i
source
@[simp]
theorem fin.cast_mk {n m : ℕ} (h : n = m) (i : ℕ) (hn : i < n) :
⇑(fin.cast h) ⟨i, hn⟩ = ⟨i, _⟩
source
@[simp]
theorem fin.cast_trans {n m k : ℕ} (h : n = m) (h' : m = k) {i : fin n} :
⇑(fin.cast h') (⇑(fin.cast h) i) = ⇑(fin.cast _) i
source
@[simp]
theorem fin.cast_refl {n : ℕ} (h : n = n := rfl) :
fin.cast h = order_iso.refl (fin n)
source
theorem fin.cast_to_equiv {n m : ℕ} (h : n = m) :
(fin.cast h).to_equiv = equiv.cast _

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

source
def fin.cast_add {n : ℕ} (m : ℕ) :
fin n ↪o fin (n + m)

cast_add m i embeds i : fin n in fin (n+m).

Equations
source
@[simp]
theorem fin.coe_cast_add {n : ℕ} (m : ℕ) (i : fin n) :
↑(⇑(fin.cast_add m) i) = ↑i
source
@[simp]
theorem fin.cast_add_mk {n : ℕ} (m i : ℕ) (h : i < n) :
⇑(fin.cast_add m) ⟨i, h⟩ = ⟨i, _⟩
source
def fin.cast_succ {n : ℕ} :
fin n ↪o fin (n + 1)

cast_succ i embeds i : fin n in fin (n+1).

Equations
source
@[simp]
theorem fin.coe_cast_succ {n : ℕ} (i : fin n) :
↑(⇑fin.cast_succ i) = ↑i
source
@[simp]
theorem fin.cast_succ_mk (n i : ℕ) (h : i < n) :
⇑fin.cast_succ ⟨i, h⟩ = ⟨i, _⟩
source
theorem fin.cast_succ_lt_succ {n : ℕ} (i : fin n) :
⇑fin.cast_succ i < i.succ
source
theorem fin.le_cast_succ_iff {n : ℕ} {i : fin (n + 1)} {j : fin n} :
i ≤ ⇑fin.cast_succ j ↔ i < j.succ
source
@[simp]
theorem fin.succ_last (n : ℕ) :
(fin.last n).succ = fin.last n.succ
source
@[simp]
theorem fin.succ_eq_last_succ {n : ℕ} (i : fin n.succ) :
i.succ = fin.last (n + 1) ↔ i = fin.last n
source
@[simp]
theorem fin.cast_succ_cast_lt {n : ℕ} (i : fin (n + 1)) (h : ↑i < n) :
⇑fin.cast_succ (i.cast_lt h) = i
source
@[simp]
theorem fin.cast_lt_cast_succ {n : ℕ} (a : fin n) (h : ↑a < n) :
(⇑fin.cast_succ a).cast_lt h = a
source
@[simp]
theorem fin.cast_succ_lt_cast_succ_iff {n : ℕ} {a b : fin n} :
⇑fin.cast_succ a < ⇑fin.cast_succ b ↔ a < b
source
theorem fin.cast_succ_injective (n : ℕ) :
function.injective ⇑fin.cast_succ
source
theorem fin.cast_succ_inj {n : ℕ} {a b : fin n} :
⇑fin.cast_succ a = ⇑fin.cast_succ b ↔ a = b
source
theorem fin.cast_succ_lt_last {n : ℕ} (a : fin n) :
⇑fin.cast_succ a < fin.last n
source
@[simp]
theorem fin.cast_succ_zero {n : ℕ} :
⇑fin.cast_succ 0 = 0
source
@[simp]
theorem fin.cast_succ_one {n : ℕ} :
⇑fin.cast_succ 1 = 1
source
theorem fin.cast_succ_pos {n : ℕ} {i : fin (n + 1)} (h : 0 < i) :
0 < ⇑fin.cast_succ i

cast_succ i is positive when i is positive

source
theorem fin.cast_succ_fin_succ (n : ℕ) (j : fin n) :
⇑fin.cast_succ j.succ = (⇑fin.cast_succ j).succ
source
@[simp, norm_cast]
theorem fin.coe_eq_cast_succ {n : ℕ} {a : fin n} :
↑a = ⇑fin.cast_succ a
source
@[simp]
theorem fin.coe_succ_eq_succ {n : ℕ} {a : fin n} :
⇑fin.cast_succ a + 1 = a.succ
source
theorem fin.lt_succ {n : ℕ} {a : fin n} :
⇑fin.cast_succ a < a.succ
source
@[simp]
theorem fin.range_cast_succ {n : ℕ} :
set.range ⇑fin.cast_succ = {i : fin (n + 1) | ↑i < n}
source
@[simp]
theorem fin.coe_of_injective_cast_succ_symm {n : ℕ} (i : fin n.succ) (hi : i ∈ set.range ⇑fin.cast_succ) :
↑(⇑((equiv.of_injective ⇑fin.cast_succ _).symm) ⟨i, hi⟩) = ↑i
source
def fin.add_nat {n : ℕ} (m : ℕ) :
fin n ↪o fin (n + m)

add_nat m i adds m to i, generalizes fin.succ.

Equations
source
@[simp]
theorem fin.coe_add_nat {n : ℕ} (m : ℕ) (i : fin n) :
↑(⇑(fin.add_nat m) i) = ↑i + m
source
def fin.nat_add (n : ℕ) {m : ℕ} :
fin m ↪o fin (n + m)

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

Equations
source
@[simp]
theorem fin.coe_nat_add (n : ℕ) {m : ℕ} (i : fin m) :
↑(⇑(fin.nat_add n) i) = n + ↑i
source
theorem fin.nat_add_zero {n : ℕ} :
fin.nat_add 0 = rel_iso.to_rel_embedding (fin.cast _)

recursion and induction principles #

source
def fin.succ_rec {C : Π (n : ℕ), fin n → Sort u_1} (H0 : Π (n : ℕ), C n.succ 0) (Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ) {n : ℕ} (i : fin n) :
C n i

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.

Equations
source
def fin.succ_rec_on {n : ℕ} (i : fin n) {C : Π (n : ℕ), fin n → Sort u_1} (H0 : Π (n : ℕ), C n.succ 0) (Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ) :
C n i

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.

A version of fin.succ_rec taking i : fin n as the first argument.

Equations
source
@[simp]
theorem fin.succ_rec_on_zero {C : Π (n : ℕ), fin n → Sort u_1} {H0 : Π (n : ℕ), C n.succ 0} {Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ} (n : ℕ) :
0.succ_rec_on H0 Hs = H0 n
source
@[simp]
theorem fin.succ_rec_on_succ {C : Π (n : ℕ), fin n → Sort u_1} {H0 : Π (n : ℕ), C n.succ 0} {Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ} {n : ℕ} (i : fin n) :
i.succ.succ_rec_on H0 Hs = Hs n i (i.succ_rec_on H0 Hs)
source
def fin.induction {n : ℕ} {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → C i.succ) (i : fin (n + 1)) :
C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

Equations
  • fin.induction h0 hs = λ (i : fin (n + 1)), subtype.cases_on i (λ (i : ℕ) (hi : i < n + 1), nat.rec (λ (hi : 0 < n + 1), _.mpr h0) (λ (i : ℕ) (IH : Π (hi : i < n + 1), C ⟨i, hi⟩) (hi : i.succ < n + 1), hs ⟨i, _⟩ (IH _)) i hi)
source
def fin.induction_on {n : ℕ} (i : fin (n + 1)) {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → C i.succ) :
C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

A version of fin.induction taking i : fin (n + 1) as the first argument.

Equations
source
def fin.cases {n : ℕ} {C : fin n.succ → Sort u_1} (H0 : C 0) (Hs : Π (i : fin n), C i.succ) (i : fin n.succ) :
C i

Define f : Π i : fin n.succ, C i by separately handling the cases i = 0 and i = j.succ, j : fin n.

Equations
source
@[simp]
theorem fin.cases_zero {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :
fin.cases H0 Hs 0 = H0
source
@[simp]
theorem fin.cases_succ {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} (i : fin n) :
fin.cases H0 Hs i.succ = Hs i
source
@[simp]
theorem fin.cases_succ' {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} {i : ℕ} (h : i + 1 < n + 1) :
fin.cases H0 Hs ⟨i.succ, h⟩ = Hs ⟨i, _⟩
source
theorem fin.forall_fin_succ {n : ℕ} {P : fin (n + 1) → Prop} :
(∀ (i : fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : fin n), P i.succ
source
theorem fin.exists_fin_succ {n : ℕ} {P : fin (n + 1) → Prop} :
(∃ (i : fin (n + 1)), P i) ↔ P 0 ∨ ∃ (i : fin n), P i.succ

pred #

source
@[simp]
theorem fin.coe_pred {n : ℕ} (j : fin (n + 1)) (h : j ≠ 0) :
↑(j.pred h) = ↑j - 1
source
@[simp]
theorem fin.succ_pred {n : ℕ} (i : fin (n + 1)) (h : i ≠ 0) :
(i.pred h).succ = i
source
@[simp]
theorem fin.pred_succ {n : ℕ} (i : fin n) {h : i.succ ≠ 0} :
i.succ.pred h = i
source
@[simp]
theorem fin.pred_mk_succ {n : ℕ} (i : ℕ) (h : i < n + 1) :
fin.pred ⟨i + 1, _⟩ _ = ⟨i, h⟩
source
theorem fin.pred_mk {n : ℕ} (i : ℕ) (h : i < n + 1) (w : ⟨i, h⟩ ≠ 0) :
fin.pred ⟨i, h⟩ w = ⟨i - 1, _⟩
source
@[simp]
theorem fin.pred_le_pred_iff {n : ℕ} {a b : fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
a.pred ha ≤ b.pred hb ↔ a ≤ b
source
@[simp]
theorem fin.pred_lt_pred_iff {n : ℕ} {a b : fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
a.pred ha < b.pred hb ↔ a < b
source
@[simp]
theorem fin.pred_inj {n : ℕ} {a b : fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0} :
a.pred ha = b.pred hb ↔ a = b
source
@[simp]
theorem fin.pred_one {n : ℕ} :
1.pred _ = 0
source
theorem fin.pred_add_one {n : ℕ} (i : fin (n + 2)) (h : ↑i < n + 1) :
(i + 1).pred _ = i.cast_lt h
source
def fin.sub_nat {n : ℕ} (m : ℕ) (i : fin (n + m)) (h : m ≤ ↑i) :
fin n

sub_nat i h subtracts m from i, generalizes fin.pred.

Equations
source
@[simp]
theorem fin.coe_sub_nat {n m : ℕ} (i : fin (n + m)) (h : m ≤ ↑i) :
↑(fin.sub_nat m i h) = ↑i - m
source
@[simp]
theorem fin.pred_cast_succ_succ {n : ℕ} (i : fin n) :
(⇑fin.cast_succ i.succ).pred _ = ⇑fin.cast_succ i
source
@[protected, instance]
def fin.has_neg (n : ℕ) :
has_neg (fin n)

Negation on fin n

Equations
source
@[protected, instance]
def fin.add_comm_group (n : ℕ) :
add_comm_group (fin (n + 1))

Abelian group structure on fin (n+1).

Equations
source
@[protected]
theorem fin.coe_neg {n : ℕ} (a : fin n) :
↑-a = (n - ↑a) % n
source
@[protected]
theorem fin.coe_sub {n : ℕ} (a b : fin n) :
↑(a - b) = (↑a + (n - ↑b)) % n
source
theorem fin.succ_above_aux {n : ℕ} (p : fin (n + 1)) :
strict_mono (λ (i : fin n), ite (⇑fin.cast_succ i < p) (⇑fin.cast_succ i) i.succ)
source
def fin.succ_above {n : ℕ} (p : fin (n + 1)) :
fin n ↪o fin (n + 1)

succ_above p i embeds fin n into fin (n + 1) with a hole around p.

Equations
source
theorem fin.succ_above_below {n : ℕ} (p : fin (n + 1)) (i : fin n) (h : ⇑fin.cast_succ i < p) :
⇑(p.succ_above) i = ⇑fin.cast_succ i

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

source
@[simp]
theorem fin.succ_above_zero {n : ℕ} :
⇑(0.succ_above) = fin.succ

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

source
@[simp]
theorem fin.succ_above_last {n : ℕ} :
(fin.last n).succ_above = fin.cast_succ

Embedding fin n into fin (n + 1) with a hole around last n embeds by cast_succ.

source
theorem fin.succ_above_last_apply {n : ℕ} (i : fin n) :
⇑((fin.last n).succ_above) i = ⇑fin.cast_succ i
source
theorem fin.succ_above_above {n : ℕ} (p : fin (n + 1)) (i : fin n) (h : p ≤ ⇑fin.cast_succ i) :
⇑(p.succ_above) 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.

source
theorem fin.succ_above_lt_ge {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑fin.cast_succ i < p ∨ p ≤ ⇑fin.cast_succ i

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

source
theorem fin.succ_above_lt_gt {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑fin.cast_succ i < p ∨ p < i.succ

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

source
@[simp]
theorem fin.succ_above_lt_iff {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑(p.succ_above) i < p ↔ ⇑fin.cast_succ 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_succ_above_iff {n : ℕ} (p : fin (n + 1)) (i : fin n) :
p < ⇑(p.succ_above) i ↔ p ≤ ⇑fin.cast_succ 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.succ_above_ne {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑(p.succ_above) 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.succ_above_pos {n : ℕ} (p : fin (n + 2)) (i : fin (n + 1)) (h : 0 < i) :
0 < ⇑(p.succ_above) i

Embedding a positive fin n results in a positive fin (n + 1)`

source
theorem fin.range_succ_above {n : ℕ} (p : fin (n + 1)) :
set.range ⇑(p.succ_above) = {i : fin (n + 1) | i ≠ p}

The range of p.succ_above is everything except p.

source
theorem fin.succ_above_right_injective {n : ℕ} {x : fin (n + 1)} :
function.injective ⇑(x.succ_above)

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

source
theorem fin.succ_above_right_inj {n : ℕ} {a b : fin n} {x : fin (n + 1)} :
⇑(x.succ_above) a = ⇑(x.succ_above) b ↔ a = b

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

source
theorem fin.succ_above_left_injective {n : ℕ} :
function.injective fin.succ_above

succ_above is injective at the pivot

source
theorem fin.succ_above_left_inj {n : ℕ} {x y : fin (n + 1)} :
x.succ_above = y.succ_above ↔ x = y

succ_above is injective at the pivot

source
@[simp]
theorem fin.zero_succ_above {n : ℕ} (i : fin n) :
⇑(0.succ_above) i = i.succ
source
@[simp]
theorem fin.succ_succ_above_zero {n : ℕ} (i : fin (n + 1)) :
⇑(i.succ.succ_above) 0 = 0
source
@[simp]
theorem fin.succ_succ_above_succ {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑(i.succ.succ_above) j.succ = (⇑(i.succ_above) j).succ
source
@[simp]
theorem fin.one_succ_above_zero {n : ℕ} :
⇑(1.succ_above) 0 = 0
source
@[simp]
theorem fin.succ_succ_above_one {n : ℕ} (i : fin (n + 2)) :
⇑(i.succ.succ_above) 1 = (⇑(i.succ_above) 0).succ

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

source
@[simp]
theorem fin.one_succ_above_succ {n : ℕ} (j : fin n) :
⇑(1.succ_above) j.succ = j.succ.succ
source
@[simp]
theorem fin.one_succ_above_one {n : ℕ} :
⇑(1.succ_above) 1 = 2
source
def fin.pred_above {n : ℕ} (p : fin n) (i : fin (n + 1)) :
fin n

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

Equations
source
theorem fin.pred_above_right_monotone {n : ℕ} (p : fin n) :
monotone p.pred_above
source
theorem fin.pred_above_left_monotone {n : ℕ} (i : fin (n + 1)) :
monotone (λ (p : fin n), p.pred_above i)
source
def fin.cast_pred {n : ℕ} (i : fin (n + 2)) :
fin (n + 1)

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

Equations
source
@[simp]
theorem fin.cast_pred_zero {n : ℕ} :
0.cast_pred = 0
source
@[simp]
theorem fin.cast_pred_one {n : ℕ} :
1.cast_pred = 1
source
@[simp]
theorem fin.pred_above_zero {n : ℕ} {i : fin (n + 2)} (hi : i ≠ 0) :
0.pred_above i = i.pred hi
source
@[simp]
theorem fin.cast_pred_last {n : ℕ} :
(fin.last (n + 1)).cast_pred = fin.last n
source
@[simp]
theorem fin.cast_pred_mk (n i : ℕ) (h : i < n + 1) :
fin.cast_pred ⟨i, _⟩ = ⟨i, h⟩
source
theorem fin.pred_above_below {n : ℕ} (p : fin (n + 1)) (i : fin (n + 2)) (h : i ≤ ⇑fin.cast_succ p) :
p.pred_above i = i.cast_pred
source
@[simp]
theorem fin.pred_above_last {n : ℕ} :
(fin.last n).pred_above = fin.cast_pred
source
theorem fin.pred_above_last_apply {n : ℕ} (i : fin n) :
(fin.last n).pred_above ↑i = ↑i.cast_pred
source
theorem fin.pred_above_above {n : ℕ} (p : fin n) (i : fin (n + 1)) (h : ⇑fin.cast_succ p < i) :
p.pred_above i = i.pred _
source
theorem fin.cast_pred_monotone {n : ℕ} :
monotone fin.cast_pred
source
@[simp]
theorem fin.succ_above_pred_above {n : ℕ} {p : fin n} {i : fin (n + 1)} (h : i ≠ ⇑fin.cast_succ p) :
⇑((⇑fin.cast_succ p).succ_above) (p.pred_above 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]
theorem fin.pred_above_succ_above {n : ℕ} (p i : fin n) :
p.pred_above (⇑((⇑fin.cast_succ p).succ_above) 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.

source
@[simp]
theorem fin.cast_pred_cast_succ {n : ℕ} (i : fin (n + 1)) :
(⇑fin.cast_succ i).cast_pred = i
source
theorem fin.cast_succ_cast_pred {n : ℕ} {i : fin (n + 2)} (h : i < fin.last (n + 1)) :
⇑fin.cast_succ i.cast_pred = i
source
theorem fin.coe_cast_pred_le_self {n : ℕ} (i : fin (n + 2)) :
↑(i.cast_pred) ≤ ↑i
source
theorem fin.coe_cast_pred_lt_iff {n : ℕ} {i : fin (n + 2)} :
↑(i.cast_pred) < ↑i ↔ i = fin.last (n + 1)
source
theorem fin.lt_last_iff_coe_cast_pred {n : ℕ} {i : fin (n + 2)} :
i < fin.last (n + 1) ↔ ↑(i.cast_pred) = ↑i
source
theorem fin.forall_iff_succ_above {n : ℕ} {p : fin (n + 1) → Prop} (i : fin (n + 1)) :
(∀ (j : fin (n + 1)), p j) ↔ p i ∧ ∀ (j : fin n), p (⇑(i.succ_above) j)
source
def fin.clamp (n m : ℕ) :
fin (m + 1)

min n m as an element of fin (m + 1)

Equations
source
@[simp]
theorem fin.coe_clamp (n m : ℕ) :
↑(fin.clamp n m) = min n m

Tuples #

We can think of the type Π(i : fin n), α i as n-tuples of elements of possibly varying type α i. A particular case is fin n → α of elements with all the same type. Here are some relevant operations, first about adding or removing elements at the beginning of a tuple.

source
@[protected, instance]
def fin.tuple0_unique (α : fin 0 → Sort u) :
unique (Π (i : fin 0), α i)

There is exactly one tuple of size zero.

Equations
source
@[simp]
theorem fin.tuple0_le {α : fin 0 → Type u_1} [Π (i : fin 0), preorder (α i)] (f g : Π (i : fin 0), α i) :
f ≤ g
source
def fin.tail {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :
α i.succ

The tail of an n+1 tuple, i.e., its last n entries.

Equations
source
theorem fin.tail_def {n : ℕ} {α : fin (n + 1) → Type u_1} {q : Π (i : fin (n + 1)), α i} :
fin.tail (λ (k : fin (n + 1)), q k) = λ (k : fin n), q k.succ
source
def fin.cons {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin (n + 1)) :
α i

Adding an element at the beginning of an n-tuple, to get an n+1-tuple.

Equations
source
@[simp]
theorem fin.tail_cons {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :
fin.tail (fin.cons x p) = p
source
@[simp]
theorem fin.cons_succ {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) :
fin.cons x p i.succ = p i
source
@[simp]
theorem fin.cons_zero {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :
fin.cons x p 0 = x
source
@[simp]
theorem fin.cons_update {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) (y : α i.succ) :
fin.cons x (function.update p i y) = function.update (fin.cons x p) i.succ y

Updating a tuple and adding an element at the beginning commute.

source
theorem fin.update_cons_zero {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (z : α 0) :
function.update (fin.cons x p) 0 z = fin.cons z p

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

source
@[simp]
theorem fin.cons_self_tail {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) :
fin.cons (q 0) (fin.tail q) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

source
@[simp]
theorem fin.tail_update_zero {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (z : α 0) :
fin.tail (function.update q 0 z) = fin.tail q

Updating the first element of a tuple does not change the tail.

source
@[simp]
theorem fin.tail_update_succ {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α i.succ) :
fin.tail (function.update q i.succ y) = function.update (fin.tail q) i y

Updating a nonzero element and taking the tail commute.

source
theorem fin.comp_cons {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (y : α) (q : fin n → α) :
g ∘ fin.cons y q = fin.cons (g y) (g ∘ q)
source
theorem fin.comp_tail {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :
g ∘ fin.tail q = fin.tail (g ∘ q)
source
theorem fin.le_cons {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {x : α 0} {q : Π (i : fin (n + 1)), α i} {p : Π (i : fin n), α i.succ} :
q ≤ fin.cons x p ↔ q 0 ≤ x ∧ fin.tail q ≤ p
source
theorem fin.cons_le {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {x : α 0} {q : Π (i : fin (n + 1)), α i} {p : Π (i : fin n), α i.succ} :
fin.cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ fin.tail q
source
@[simp]
theorem fin.range_cons {α : Type u_1} {n : ℕ} (x : α) (b : fin n → α) :
set.range (fin.cons x b) = insert x (set.range b)
source
def fin.append {n m : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : fin m → α) (v : fin n → α) :
fin o → α

fin.append ho u v appends two vectors of lengths m and n to produce one of length o = m + n. ho provides control of definitional equality for the vector length.

Equations
source
@[simp]
theorem fin.fin_append_apply_zero {n m : ℕ} {α : Type u_1} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : fin (m + 1) → α) (v : fin n → α) :
fin.append ho u v 0 = u 0

In the previous section, we have discussed inserting or removing elements on the left of a tuple. In this section, we do the same on the right. A difference is that fin (n+1) is constructed inductively from fin n starting from the left, not from the right. This implies that Lean needs more help to realize that elements belong to the right types, i.e., we need to insert casts at several places.

source
def fin.init {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :
α (⇑fin.cast_succ i)

The beginning of an n+1 tuple, i.e., its first n entries

Equations
source
theorem fin.init_def {n : ℕ} {α : fin (n + 1) → Type u_1} {q : Π (i : fin (n + 1)), α i} :
fin.init (λ (k : fin (n + 1)), q k) = λ (k : fin n), q (⇑fin.cast_succ k)
source
def fin.snoc {n : ℕ} {α : fin (n + 1) → Type u} (p : Π (i : fin n), α (⇑fin.cast_succ i)) (x : α (fin.last n)) (i : fin (n + 1)) :
α i

Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

Equations
source
@[simp]
theorem fin.init_snoc {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α (⇑fin.cast_succ i)) :
fin.init (fin.snoc p x) = p
source
@[simp]
theorem fin.snoc_cast_succ {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α (⇑fin.cast_succ i)) (i : fin n) :
fin.snoc p x (⇑fin.cast_succ i) = p i
source
@[simp]
theorem fin.snoc_last {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α (⇑fin.cast_succ i)) :
fin.snoc p x (fin.last n) = x
source
@[simp]
theorem fin.snoc_update {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α (⇑fin.cast_succ i)) (i : fin n) (y : α (⇑fin.cast_succ i)) :
fin.snoc (function.update p i y) x = function.update (fin.snoc p x) (⇑fin.cast_succ i) y

Updating a tuple and adding an element at the end commute.

source
theorem fin.update_snoc_last {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α (⇑fin.cast_succ i)) (z : α (fin.last n)) :
function.update (fin.snoc p x) (fin.last n) z = fin.snoc p z

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

source
@[simp]
theorem fin.snoc_init_self {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) :
fin.snoc (fin.init q) (q (fin.last n)) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

source
@[simp]
theorem fin.init_update_last {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (z : α (fin.last n)) :
fin.init (function.update q (fin.last n) z) = fin.init q

Updating the last element of a tuple does not change the beginning.

source
@[simp]
theorem fin.init_update_cast_succ {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α (⇑fin.cast_succ i)) :
fin.init (function.update q (⇑fin.cast_succ i) y) = function.update (fin.init q) i y

Updating an element and taking the beginning commute.

source
theorem fin.tail_init_eq_init_tail {n : ℕ} {β : Type u_1} (q : fin (n + 2) → β) :
fin.tail (fin.init q) = fin.init (fin.tail q)

tail and init commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

source
theorem fin.cons_snoc_eq_snoc_cons {n : ℕ} {β : Type u_1} (a : β) (q : fin n → β) (b : β) :
fin.cons a (fin.snoc q b) = fin.snoc (fin.cons a q) b

cons and snoc commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

source
theorem fin.comp_snoc {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n → α) (y : α) :
g ∘ fin.snoc q y = fin.snoc (g ∘ q) (g y)
source
theorem fin.comp_init {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :
g ∘ fin.init q = fin.init (g ∘ q)
source
def fin.insert_nth' {n : ℕ} {α : fin (n + 2) → Type u} (i : fin (n + 2)) (x : α i) (p : Π (j : fin (n + 1)), α (⇑(i.succ_above) j)) (j : fin (n + 2)) :
α j

Insert an element into a tuple at a given position, auxiliary definition. For the general definition, see insert_nth.

Equations
source
def fin.insert_nth {n : ℕ} {α : fin (n + 1) → Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α (⇑(i.succ_above) j)) (j : fin (n + 1)) :
α j

Insert an element into a tuple at a given position. For i = 0 see fin.cons, for i = fin.last n see fin.snoc.

Equations
source
@[simp]
theorem fin.insert_nth_apply_same {n : ℕ} {α : fin (n + 1) → Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α (⇑(i.succ_above) j)) :
i.insert_nth x p i = x
source
@[simp]
theorem fin.insert_nth_apply_succ_above {n : ℕ} {α : fin (n + 1) → Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α (⇑(i.succ_above) j)) (j : fin n) :
i.insert_nth x p (⇑(i.succ_above) j) = p j
source
@[simp]
theorem fin.insert_nth_comp_succ_above {n : ℕ} {β : Type v} (i : fin (n + 1)) (x : β) (p : fin n → β) :
i.insert_nth x p ∘ ⇑(i.succ_above) = p
source
theorem fin.insert_nth_eq_iff {n : ℕ} {α : fin (n + 1) → Type u} {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α (⇑(i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
i.insert_nth x p = q ↔ q i = x ∧ p = λ (j : fin n), q (⇑(i.succ_above) j)
source
theorem fin.eq_insert_nth_iff {n : ℕ} {α : fin (n + 1) → Type u} {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α (⇑(i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
q = i.insert_nth x p ↔ q i = x ∧ p = λ (j : fin n), q (⇑(i.succ_above) j)
source
theorem fin.insert_nth_zero {n : ℕ} {α : fin (n + 1) → Type u} (x : α 0) (p : Π (j : fin n), α (⇑(0.succ_above) j)) :
0.insert_nth x p = fin.cons x (λ (j : fin n), cast _ (p j))
source
@[simp]
theorem fin.insert_nth_zero' {n : ℕ} {β : Type v} (x : β) (p : fin n → β) :
0.insert_nth x p = fin.cons x p
source
theorem fin.insert_nth_last {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (j : fin n), α (⇑((fin.last n).succ_above) j)) :
(fin.last n).insert_nth x p = fin.snoc (λ (j : fin n), cast _ (p j)) x
source
@[simp]
theorem fin.insert_nth_last' {n : ℕ} {β : Type v} (x : β) (p : fin n → β) :
(fin.last n).insert_nth x p = fin.snoc p x
source
theorem fin.insert_nth_le_iff {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α (⇑(i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
i.insert_nth x p ≤ q ↔ x ≤ q i ∧ p ≤ λ (j : fin n), q (⇑(i.succ_above) j)
source
theorem fin.le_insert_nth_iff {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α (⇑(i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
q ≤ i.insert_nth x p ↔ q i ≤ x ∧ (λ (j : fin n), q (⇑(i.succ_above) j)) ≤ p
source
theorem fin.insert_nth_mem_Icc {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α (⇑(i.succ_above) j)} {q₁ q₂ : Π (j : fin (n + 1)), α j} :
i.insert_nth x p ∈ set.Icc q₁ q₂ ↔ x ∈ set.Icc (q₁ i) (q₂ i) ∧ p ∈ set.Icc (λ (j : fin n), q₁ (⇑(i.succ_above) j)) (λ (j : fin n), q₂ (⇑(i.succ_above) j))
source
theorem fin.preimage_insert_nth_Icc_of_mem {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {q₁ q₂ : Π (j : fin (n + 1)), α j} (hx : x ∈ set.Icc (q₁ i) (q₂ i)) :
i.insert_nth x ⁻¹' set.Icc q₁ q₂ = set.Icc (λ (j : fin n), q₁ (⇑(i.succ_above) j)) (λ (j : fin n), q₂ (⇑(i.succ_above) j))
source
theorem fin.preimage_insert_nth_Icc_of_not_mem {n : ℕ} {α : fin (n + 1) → Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {q₁ q₂ : Π (j : fin (n + 1)), α j} (hx : x ∉ set.Icc (q₁ i) (q₂ i)) :
i.insert_nth x ⁻¹' set.Icc q₁ q₂ = ∅
source
def fin.find {n : ℕ} (p : fin n → Prop) [decidable_pred p] :
option (fin n)

find p returns the first index n where p n is satisfied, and none if it is never satisfied.

Equations
source
theorem fin.find_spec {n : ℕ} (p : fin n → Prop) [decidable_pred p] {i : fin n} (hi : i ∈ fin.find p) :
p i

If find p = some i, then p i holds

source
theorem fin.is_some_find_iff {n : ℕ} {p : fin n → Prop} [decidable_pred p] :
↥((fin.find p).is_some) ↔ ∃ (i : fin n), p i

find p does not return none if and only if p i holds at some index i.

source
theorem fin.find_eq_none_iff {n : ℕ} {p : fin n → Prop} [decidable_pred p] :
fin.find p = none ↔ ∀ (i : fin n), ¬p i

find p returns none if and only if p i never holds.

source
theorem fin.find_min {n : ℕ} {p : fin n → Prop} [decidable_pred p] {i : fin n} (hi : i ∈ fin.find p) {j : fin n} (hj : j < i) :
¬p j

If find p returns some i, then p j does not hold for j < i, i.e., i is minimal among the indices where p holds.

source
theorem fin.find_min' {n : ℕ} {p : fin n → Prop} [decidable_pred p] {i : fin n} (h : i ∈ fin.find p) {j : fin n} (hj : p j) :
i ≤ j
source
theorem fin.nat_find_mem_find {n : ℕ} {p : fin n → Prop} [decidable_pred p] (h : ∃ (i : ℕ) (hin : i < n), p ⟨i, hin⟩) :
⟨nat.find h, _⟩ ∈ fin.find p
source
theorem fin.mem_find_iff {n : ℕ} {p : fin n → Prop} [decidable_pred p] {i : fin n} :
i ∈ fin.find p ↔ p i ∧ ∀ (j : fin n), p j → i ≤ j
source
theorem fin.find_eq_some_iff {n : ℕ} {p : fin n → Prop} [decidable_pred p] {i : fin n} :
fin.find p = some i ↔ p i ∧ ∀ (j : fin n), p j → i ≤ j
source
theorem fin.mem_find_of_unique {n : ℕ} {p : fin n → Prop} [decidable_pred p] (h : ∀ (i j : fin n), p i → p j → i = j) {i : fin n} (hi : p i) :
i ∈ fin.find p
source
@[simp]
theorem fin.coe_of_nat_eq_mod (m n : ℕ) :
↑↑n = n % m.succ
source
@[simp]
theorem fin.coe_of_nat_eq_mod' (m n : ℕ) [I : fact (0 < m)] :
↑(fin.of_nat' n) = n % m

mul #

source
theorem fin.val_mul {n : ℕ} (a b : fin n) :
(a * b).val = (a.val) * b.val % n
source
theorem fin.coe_mul {n : ℕ} (a b : fin n) :
↑a * b = (↑a) * ↑b % n
source
@[protected, simp]
theorem fin.mul_one {n : ℕ} (k : fin (n + 1)) :
k * 1 = k
source
@[protected, simp]
theorem fin.one_mul {n : ℕ} (k : fin (n + 1)) :
1 * k = k
source
@[protected, simp]
theorem fin.mul_zero {n : ℕ} (k : fin (n + 1)) :
k * 0 = 0
source
@[protected, simp]
theorem fin.zero_mul {n : ℕ} (k : fin (n + 1)) :
0 * k = 0