File/folder structure vs namespaces

Stream: lean4

[Yuri de Wit]

I am trying to wrap my head around how one would structure a package in Lean4 consisting of multiple, nested namespaces. But after looking at a few projects I am still unsure.

Is there a best practice considering that Lean seems to be quite flexible here (from all namespaces in single file all the way to at most one namespace per file) and I don't see a strong consistency across a few different packages I looked at?