Commit 2024-02-07 22:43 8d817bbe

View on Github →

feat(Data/Fin/OrderHom): Factor out succAbove and predAbove from Data.Fin.Basic. (#10166) Move succAbove and predAbove to their own file, updating their documentation and adding an OrderHom instance for predAbove, predAboveOrderHom.

Estimated changes

deleted theorem Fin.castPred_succAbove
deleted theorem Fin.exists_succAbove_eq
deleted theorem Fin.ne_succAbove
deleted theorem Fin.one_succAbove_one
deleted theorem Fin.one_succAbove_succ
deleted theorem Fin.one_succAbove_zero
deleted def Fin.predAbove
deleted theorem Fin.predAbove_last_apply
deleted theorem Fin.predAbove_of_lt_succ
deleted theorem Fin.predAbove_of_succ_le
deleted theorem Fin.predAbove_pred_of_le
deleted theorem Fin.predAbove_pred_of_lt
deleted theorem Fin.predAbove_pred_self
deleted theorem Fin.predAbove_rev_left
deleted theorem Fin.predAbove_rev_right
deleted theorem Fin.predAbove_right_last
deleted theorem Fin.predAbove_right_zero
deleted theorem Fin.predAbove_succAbove
deleted theorem Fin.predAbove_succ_of_le
deleted theorem Fin.predAbove_succ_of_lt
deleted theorem Fin.predAbove_succ_self
deleted theorem Fin.predAbove_zero
deleted theorem Fin.predAbove_zero_succ
deleted theorem Fin.pred_succAbove
deleted theorem Fin.pred_succAbove_pred
deleted theorem Fin.range_succ
deleted theorem Fin.range_succAbove
deleted theorem Fin.rev_predAbove
deleted theorem Fin.rev_succAbove
deleted theorem Fin.strictMono_succAbove
deleted def Fin.succAbove
deleted def Fin.succAboveEmb
deleted theorem Fin.succAbove_eq_last_iff
deleted theorem Fin.succAbove_eq_zero_iff
deleted theorem Fin.succAbove_last
deleted theorem Fin.succAbove_last_apply
deleted theorem Fin.succAbove_left_inj
deleted theorem Fin.succAbove_lt_ge
deleted theorem Fin.succAbove_ne
deleted theorem Fin.succAbove_ne_last
deleted theorem Fin.succAbove_ne_zero
deleted theorem Fin.succAbove_of_lt_succ
deleted theorem Fin.succAbove_of_succ_le
deleted theorem Fin.succAbove_pos
deleted theorem Fin.succAbove_predAbove
deleted theorem Fin.succAbove_pred_of_le
deleted theorem Fin.succAbove_pred_of_lt
deleted theorem Fin.succAbove_pred_self
deleted theorem Fin.succAbove_rev_left
deleted theorem Fin.succAbove_rev_right
deleted theorem Fin.succAbove_right_inj
deleted theorem Fin.succAbove_succ_of_le
deleted theorem Fin.succAbove_succ_of_lt
deleted theorem Fin.succAbove_succ_self
deleted theorem Fin.succAbove_zero
deleted theorem Fin.succAbove_zero_apply
deleted theorem Fin.succ_predAbove_succ
deleted theorem Fin.succ_predAbove_zero
deleted theorem Fin.succ_succAbove_one
deleted theorem Fin.succ_succAbove_succ
deleted theorem Fin.succ_succAbove_zero
deleted theorem Fin.zero_succAbove
added theorem Fin.castPred_succAbove
added theorem Fin.ne_succAbove
added theorem Fin.one_succAbove_one
added theorem Fin.one_succAbove_succ
added theorem Fin.one_succAbove_zero
added def Fin.predAbove
added theorem Fin.predAbove_rev_left
added theorem Fin.predAbove_zero
added theorem Fin.pred_succAbove
added theorem Fin.range_succ
added theorem Fin.range_succAbove
added theorem Fin.rev_predAbove
added theorem Fin.rev_succAbove
added def Fin.succAbove
added def Fin.succAboveEmb
added theorem Fin.succAbove_last
added theorem Fin.succAbove_left_inj
added theorem Fin.succAbove_lt_ge
added theorem Fin.succAbove_ne
added theorem Fin.succAbove_ne_last
added theorem Fin.succAbove_ne_zero
added theorem Fin.succAbove_pos
added theorem Fin.succAbove_rev_left
added theorem Fin.succAbove_zero
added theorem Fin.succ_succAbove_one
added theorem Fin.zero_succAbove