## Stream: general

### Topic: Terminology

#### Sebastien Gouezel (Feb 05 2019 at 13:15):

The following lemma is missing in the library

theorem to_nat_le_to_nat_of_le {a b : ℤ} (h : a ≤ b) : to_nat a ≤ to_nat b :=
by rw to_nat_le; exact le_trans h (le_to_nat b)


Should I call it to_nat_le_to_nat_of_le, or to_nat_mono? There are several lemmas named foo_mono in the library, but for uniformity I tend to prefer to_nat_le_to_nat_of_le (and I would be happy if all mono lemmas were renamed analogously). Strong opinions on this?

#### Mario Carneiro (Feb 05 2019 at 13:35):

I would go for to_nat_le, to_nat_le_to_nat, or to_nat_mono

#### Mario Carneiro (Feb 05 2019 at 13:35):

depending on whether there are any other reasonable similar theorems

#### Mario Carneiro (Feb 05 2019 at 13:37):

I'm not a fan of names that are considerably longer than needed for disambiguation

#### Sebastien Gouezel (Feb 05 2019 at 13:40):

OK, let's go for to_nat_le_to_nat (I don't like to_nat_mono because the natural thing to do is to start with to_nat_le and ask for autocompletion, which will fail).

#### Mario Carneiro (Feb 05 2019 at 13:43):

If it is a problem we can also have aliases, although we don't use them too often

Last updated: May 09 2021 at 18:17 UTC