Introducing myself + Naming Conventions

Stream: new members

[David Blitz]

I'm David a hobby mathematician from Berlin, DE. I finished the Natural Number Game in my web browser and just installed lean to play the lost levels.
I've got a quick question concerning the Natural Number Game:
In

theorem lt_of_lt_of_le {a b c : mynat} : a < b → b ≤ c → a < c :=

and in similar definitions,
why is an 'arrow' between types translated to '_of_' in natural language?

[Damiano Testa]

Hi!

"Consequence of", maybe?

[Eric Wieser]

I assume the rationale is similar to how person -> name could be called name_of_person.

[David Blitz]

Oh true, that makes sense. I think, I was confused by the translation switching 'source' and 'target' of the 'arrow'. I guess you could say I was expecting a co-variant translation ;) Is this a standard convention in lean?

[Rémy Degenne]

AFAIK, the standard convention is to name your theorem by its conclusion. The _of_ and the hypotheses are often absent if they are obvious

[Ruben Van de Velde]

And yeah, "of" is a standard mathlib #naming convention

[Mario Carneiro]

I read it more like "from", although I grant that the prepositions are not interchangeable

[Mario Carneiro]

mostly it's just a naming convention because if was taken

[Mario Carneiro]

and it pays to be short because this is certainly the number 1 most common label segment in mathlib

[Kevin Buzzard]

I was always confused about why A_of_B_of_C meant B -> C -> A but actually when it comes to writing code this convention does seem to work quite well, you always know your goal and then you think of the hypotheses in order

[David Blitz]

@Kevin Buzzard Maybe it could be beneficial to explain this naming convention and its quirks in the Natural Number Game when it first pops up? (I think in Level 8 of Advanced Addition World)

[Kevin Buzzard]

The whole game needs a tidy-up really. I just leave it because currently it works well enough and I'm busy with other projects. I wrote it because I was teaching this stuff.

[David Blitz]

I have to say that I really enjoyed the game as it is already. But I'll maybe create an issue for an explanation of the '_of_' naming convention in the game on github.