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
def fin.lt {n : } (a b : fin n) :
Prop

Equations
def fin.le {n : } (a b : fin 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} (h : i.val j.val) :
i j

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

@[instance]

Equations