mathlib documentation

core.init.data.fin.basic

def fin  :
→ Type

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

Equations
def fin.mk {n : } (i : ) :
i < nfin n

Backwards-compatible constructor for fin n.

Equations
def fin.lt {n : } :
fin nfin n → Prop

Equations
def fin.le {n : } :
fin nfin n → Prop

Equations
@[instance]
def fin.has_lt {n : } :

Equations
@[instance]
def fin.has_le {n : } :

Equations
@[instance]
def fin.decidable_lt {n : } (a b : fin n) :
decidable (a < b)

Equations
@[instance]
def fin.decidable_le {n : } (a b : fin n) :

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

Equations
theorem fin.eq_of_veq {n : } {i j : fin n} :
i.val = j.vali = j

theorem fin.veq_of_eq {n : } {i j : fin n} :
i = ji.val = j.val

theorem fin.ne_of_vne {n : } {i j : fin n} :
i.val j.vali j

theorem fin.vne_of_ne {n : } {i j : fin n} :
i ji.val j.val

@[instance]

Equations