Fin.succAbove_inj vs Fin.succAbove_right_inj

Stream: mathlib4

[Yury G. Kudryashov]

Which name should survive and which one should be deprecated?

[Bhavik Mehta]

docs#Fin.succAbove_inj; docs#Fin.succAbove_right_inj

[Joël Riou]

I would rather keep Fin.succAbove_inj: this is the injectivity of the map p.succAbove : Fin n → Fin (n + 1).

[Aaron Liu]

Then what should injectivity of Fin.succAbove : Fin (n + 1) → (Fin n → Fin (n + 1)) be called?

[Yury G. Kudryashov]

To compare, see docs#Fin.succAbove_left_inj

[Yury G. Kudryashov]

I think I agree with "myFun_inj" means injectivity of the fully applied function, if it's true".

[Yury G. Kudryashov]

But I'm going to wait for more opinions.