# Zulip Chat Archive

## 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