Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 13:50 d2b39404

View on Github →

feat(data/fin): ascend / descend for fin

Estimated changes

Modified data/fin.lean

deleted theorem eq_of_lt_succ_of_not_lt

added def fin.ascend

added theorem fin.ascend_descend

added theorem fin.ascend_ne

modified def fin.cases

modified theorem fin.cases_succ

modified theorem fin.cases_zero

added def fin.descend

added theorem fin.descend_ascend

added theorem fin.eq_of_lt_succ_of_not_lt

added theorem fin.fin.raise_val

added def fin.fin_zero_elim

added def fin.lower

added def fin.lower_left

added def fin.lower_right

added theorem fin.lower_val

added theorem fin.pred_succ

added theorem fin.raise_lower

added def fin.raise_nat

added theorem fin.raise_val

added theorem fin.succ_pred

modified def fin.succ_rec

modified def fin.succ_rec_on

modified theorem fin.succ_rec_on_succ

modified theorem fin.succ_rec_on_zero

deleted def lower_left

deleted def lower_right

deleted def raise_nat