Commit 2024-05-30 11:57 c6db3cce

View on Github →

chore: Delete Data.Fin.OrderHom (#13147) Move the content of Data.Fin.OrderHom to

  • Data.Fin.Basic for the definitions and almost all lemmas
  • Order.Fin for the order properties For this to not be terribly painful, I had to prove a few Fin-specific basic order lemmas.

Estimated changes

added theorem Fin.castPred_succAbove
added theorem Fin.coe_succAboveEmb
added theorem Fin.ne_last_of_lt
added theorem Fin.ne_succAbove
added theorem Fin.ne_zero_of_lt
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
deleted theorem Fin.castPred_succAbove
deleted theorem Fin.coe_succAboveEmb
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