Commit 2024-01-16 19:40 34368d1e

View on Github →

fix(Data/Fin/Basic): castPred consistency redefinition. (#9780) This PR redefines castPred to be more consistent with the definition of both pred and castSucc, so that the relationship between castSucc and castPred and succ and pred becomes exactly analogous. It also adds some supplementary and analogous lemmas designed to facilitate this. As castPred is no longer dependent on predAbove, its definition is moved to a more appropriate place.

Estimated changes

added theorem Fin.castLT_eq_castPred
modified def Fin.castPred
modified theorem Fin.castPred_castSucc
added theorem Fin.castPred_inj
deleted theorem Fin.castPred_last
added theorem Fin.castPred_le_iff
added theorem Fin.castPred_lt_iff
deleted theorem Fin.castPred_mk'
modified theorem Fin.castPred_mk
deleted theorem Fin.castPred_monotone
modified theorem Fin.castPred_one
added theorem Fin.castPred_zero'
modified theorem Fin.castPred_zero
modified theorem Fin.castSucc_castPred
added theorem Fin.castSucc_pred_lt
modified theorem Fin.coe_castPred
deleted theorem Fin.coe_castPred_le_self
deleted theorem Fin.coe_castPred_lt_iff
added theorem Fin.last_pos'
added theorem Fin.le_castPred_iff
added theorem Fin.le_pred_iff
added theorem Fin.lt_castPred_iff
added theorem Fin.lt_castPred_succ
added theorem Fin.lt_pred_iff
added theorem Fin.lt_succ_castPred
added theorem Fin.one_lt_last
added theorem Fin.one_pos'
modified theorem Fin.predAbove_below
deleted theorem Fin.predAbove_last
modified theorem Fin.predAbove_last_apply
added theorem Fin.pred_castSucc_lt
added theorem Fin.pred_last
added theorem Fin.pred_le_iff
added theorem Fin.pred_lt_castPred
added theorem Fin.pred_lt_iff
added theorem Fin.pred_one'
added theorem Fin.rev_castPred
added theorem Fin.rev_eq_iff
added theorem Fin.rev_ne_iff
added theorem Fin.rev_pred
added theorem Fin.succ_ne_last_iff
added theorem Fin.zero_ne_one'