# mathlibdocumentation

core / init.data.fin.basic

structure fin (n : ) :
Type
• val :
• property : self.val < n

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

Instances for fin
@[protected]
def fin.lt {n : } (a b : fin n) :
Prop
Equations
@[protected]
def fin.le {n : } (a b : fin n) :
Prop
Equations
@[protected, instance]
def fin.has_lt {n : } :
Equations
@[protected, instance]
def fin.has_le {n : } :
Equations
@[protected, instance]
def fin.decidable_lt {n : } (a b : fin n) :
decidable (a < b)
Equations
@[protected, 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} (h : i.val j.val) :
i j
theorem fin.vne_of_ne {n : } {i j : fin n} (h : i j) :
i.val j.val
@[protected, instance]
Equations
• = λ (i j : fin n),