how to organize extra lemmas

Stream: general

[Bernd Losert]

I am developing a library formalizing the theory of convergence spaces. In doing so, I have needed a bunch of lemmas that don't have to do with convergence spaces. I usually put these lemmas near the code that is using them, but sometimes I need the lemmas in other places and so I am wondering about how to best organize this. Ideally, I would have all these lemmas be part of mathlib. In fact, I already managed to get a bunch of them in mathlib, but some are not "general" enough for mathlib.

Question: Where should I put these extra lemmas that are not part of the main theory? The best idea I have so far is to just make an extras module and dump the lemmas there. What do other people usually do?

[Yaël Dillies]

What I do is to have a dump file .mathlib where I put all the preliminary lemmas. Coincidentally, it also serves as a kitchen sink import.

[Yaël Dillies]

See for example branch#szemeredi, branch#polytopes or branch#sperner-again.

[Bernd Losert]

All your examples are branches of mathlib. Where are the .mathlib dump files you speak of?

[Bernd Losert]

I guess I could just make my own branch of mathlib and organize my lemmas in there.

[Yaël Dillies]

You can compare through Github, but it is here https://github.com/leanprover-community/mathlib/blob/szemeredi/src/combinatorics/szemeredi/mathlib.lean

[Bernd Losert]

I see.