core / init.data.fin.basic

source

def fin (n : ℕ) :

Type

fin n is the subtype of ℕ consisting of natural numbers strictly smaller than n.

Equations

fin n = {i // i < n}

source

def fin.mk {n : ℕ} (i : ℕ) (h : i < n) :

fin n

Backwards-compatible constructor for fin n.

Equations

fin.mk i h = ⟨i, h⟩

source

@[protected]

def fin.lt {n : ℕ} (a b : fin n) :

Prop

Equations

a.lt b = (a.val < b.val)

source

@[protected]

def fin.le {n : ℕ} (a b : fin n) :

Prop

Equations

a.le b = (a.val ≤ b.val)

source

@[protected, instance]

def fin.has_lt {n : ℕ} :

has_lt (fin n)

Equations

fin.has_lt = {lt := fin.lt n}

source

@[protected, instance]

def fin.has_le {n : ℕ} :

has_le (fin n)

Equations

fin.has_le = {le := fin.le n}

source

@[protected, instance]

def fin.decidable_lt {n : ℕ} (a b : fin n) :

decidable (a < b)

Equations

a.decidable_lt b = a.val.decidable_lt b.val

source

@[protected, instance]

def fin.decidable_le {n : ℕ} (a b : fin n) :

decidable (a ≤ b)

Equations

a.decidable_le b = a.val.decidable_le b.val

source

def fin.elim0 {α : fin 0 → Sort u} (x : fin 0) :

α x

Equations

fin.elim0 ⟨n, h⟩ = absurd h _

source

theorem fin.eq_of_veq {n : ℕ} {i j : fin n} :

i.val = j.val → i = j

source

theorem fin.veq_of_eq {n : ℕ} {i j : fin n} :

i = j → i.val = j.val

source

theorem fin.ne_of_vne {n : ℕ} {i j : fin n} (h : i.val ≠ j.val) :

i ≠ j

source

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

i.val ≠ j.val

source

@[protected, instance]

def fin.decidable_eq (n : ℕ) :

decidable_eq (fin n)

Equations

fin.decidable_eq n = λ (i j : fin n), decidable_of_decidable_of_iff (nat.decidable_eq i.val j.val) _