Commit 2024-02-07 04:38 2fe4a57d

View on Github →

feat(Data/Fin/Basic): Rename and extend *_above and _below lemmas (#10163) Rename succAbove_below, succAbove_above, predAbove_below and predAbove_Above to more appropriate things, and vary and extend these results to allow for faster proofs elsewhere.

Estimated changes

deleted theorem Fin.castLT_succAbove
added theorem Fin.castPred_succAbove
added theorem Fin.exists_succ_eq
deleted theorem Fin.exists_succ_eq_iff
added theorem Fin.le_rev_iff
added theorem Fin.lt_rev_iff
deleted theorem Fin.lt_succAbove_iff
deleted theorem Fin.predAbove_above
deleted theorem Fin.predAbove_below
added theorem Fin.predAbove_rev_left
modified theorem Fin.predAbove_zero
modified theorem Fin.pred_succAbove
added theorem Fin.rev_le_iff
added theorem Fin.rev_lt_iff
deleted theorem Fin.succAbove_above
deleted theorem Fin.succAbove_below
deleted theorem Fin.succAbove_castLT
deleted theorem Fin.succAbove_lt_iff
deleted theorem Fin.succAbove_pred
added theorem Fin.succAbove_rev_left
added theorem Fin.succ_ne_last_of_lt