mathlib3 documentation

core / init.data.fin.basic

@[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 0 Sort u} (x : fin 0) :
α x
Equations
theorem fin.eq_of_veq {n : } {i j : fin n} :
i.val = j.val i = j
theorem fin.veq_of_eq {n : } {i j : fin n} :
i = j i.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