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 #

finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0. Further definitions and eliminators can be found in Init.Data.Fin.Lemmas
Fin.equivSubtype : Equivalence between Fin n and { i // i < n }.

source

theorem Nat.forall_lt_iff_fin {n : ℕ} {p : (k : ℕ) → k < n → Prop} :

(∀ (k : ℕ) (hk : k < n), p k hk) ↔ ∀ (k : Fin n), p ↑k ⋯

source

theorem Nat.exists_lt_iff_fin {n : ℕ} {p : (k : ℕ) → k < n → Prop} :

(∃ (k : ℕ ), ∃ (hk : k < n), p k hk) ↔ ∃ (k : Fin n), p ↑k ⋯

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 = x.elim0

Instances For

source

@[simp]

theorem Fin.mk_eq_one {n a : ℕ} {ha : a < n + 2} :

⟨a, ha⟩ = 1 ↔ a = 1

source

@[simp]

theorem Fin.one_eq_mk {n a : ℕ} {ha : a < n + 2} :

1 = ⟨a, ha⟩ ↔ a = 1

source

instance Fin.instCanLiftNatValLt {n : ℕ} :

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

source

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

α i

A dependent variant of Fin.elim0.

Equations

i.rec0 = absurd ⋯ ⋯

Instances For

source

theorem Fin.val_injective {n : ℕ} :

Function.Injective val

source

theorem Fin.size_positive {n : ℕ} :

∀ (a : 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

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

a < last n ↔ a ≠ last n

source

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

b ≠ 0

source

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

a ≠ last n

source

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 := ⋯ }

Instances For

source

@[simp]

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

equivSubtype a = ⟨↑a, ⋯⟩

source

@[simp]

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

equivSubtype.symm a = ⟨↑a, ⋯⟩

source

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

NeZero n

coercions and constructions #

source

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

↑a = ↑b ↔ a = b

source

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

a ≠ b ↔ ↑a ≠ ↑b

source

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

⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

source

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

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' → α} :

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

source

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

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 #

source

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

a < b ∨ b ≤ a

Fin.lt_or_ge is an alias of Fin.lt_or_le. It is preferred since it follows the mathlib naming convention.

source

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

a ≤ b ∨ b < a

Fin.le_or_gt is an alias of Fin.le_or_lt. It is preferred since it follows the mathlib naming convention.

source

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

a ≤ b ↔ ↑a ≤ ↑b

source

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

source

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

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

@[implicit_reducible]

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

source

@[simp]

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

⟨0, ⋯⟩ = 0

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

source

@[simp]

theorem Fin.val_pos_iff {n : ℕ} [NeZero n] {a : Fin n} :

0 < ↑a ↔ 0 < a

source

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.

source

@[simp]

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

Fin.cast ⋯ a = a

source

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

source

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

Function.Injective (Fin.cast h)

source

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

0 < last n

source

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

1 < last (n + 1)

Coercions to `ℤ` and the `fin_omega` tactic. #

source

theorem Fin.coe_int_sub_eq_ite {n : ℕ} (u v : Fin n) :

↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

source

theorem Fin.coe_int_sub_eq_mod {n : ℕ} (u v : Fin n) :

↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

source

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

source

theorem Fin.coe_int_add_eq_mod {n : ℕ} (u v : Fin n) :

↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

source

def Fin.tacticFin_omega :

Lean.ParserDescr

fin_omega is a preprocessor for omega to handle inequalities in Fin. It rewrites all hypotheses and the goal, turning statements about addition, subtraction and inequalities in Fin n into statements that omega can use/solve. Note that this involves a lot of case splitting, so may be slow.

Equations