mathlib documentation

core / init.data.fin.basic

def fin (n : ) :
Type

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

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

Backwards-compatible constructor for fin n.

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