Naming convention: f (k + 1) <= f k + 1

Stream: lean4

[Siddharth Bhat]

Consider the theorem:

theorem foo {k : Nat} {f : Nat → Nat} : f (k + 1) ≤ f k + 1 := sorry

What's the name of this theorem supposed to be? As far as I can tell, the "naming algorithm" says f_succ_le_f_succ, which is a bit nonsensical :)

[Floris van Doorn]

I assume you're asking this in the case that f is a specific function/declaration? Yes, our naming convention would indeed prescribe the name you suggest, but there is some flexibility. It would be easier if there is a mathematical term for this behavior "f - id is non-increasing", and then just use that term (in the same way, add_comm is not called add_eq_add).

[Sabbir Rahman]

That will probably be named f_succ_le_succ_f since in rhs, the succ happens after applying f.

[Ruben Van de Velde]

Sounds more like f_add_one_le_f_add_one