Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 07:54 5258de08

View on Github →

feat(data/fin): refactor pred_above (#6125) Currently the signature of pred_above is

def pred_above (p : fin (n+1)) (i : fin (n+1)) (hi : i ≠ p) : fin n := ...

and its behaviour is "subtract one from i if it is greater than p". There are two reasons I don't like this much:

  1. It's not a total function.
  2. Since succ_above is exactly a simplicial face map, I'd like pred_above to be a simplicial degeneracy map. In this PR I propose replacing this with
def pred_above (p : fin n) (i : fin (n+1)) : fin n :=

again with the behaviour "subtract one from i if it is greater than p". ~~Unfortunately, it seems the current pred_above really is needed for the sake of fin.insert_nth, so this PR has ended up as a half-hearted attempt to replace pred_above

Estimated changes

added def fin.cast_pred
added theorem fin.cast_pred_last
added theorem fin.cast_pred_mk
added theorem fin.cast_pred_zero
modified theorem fin.cast_succ_mk
added def fin.insert_nth'
modified def fin.insert_nth
added theorem fin.is_le
added theorem fin.le_cast_succ_iff
added theorem fin.pos_iff_ne_zero
modified def fin.pred_above
modified theorem fin.pred_above_succ_above
modified theorem fin.pred_above_zero
added theorem fin.range_succ_above
modified theorem fin.succ_above_pred_above