Commit 2023-05-30 23:18 32837559

chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129) This PR is a revision of #19122: it addresses namespacing in archive and counterexamples. The main difference with #19122 is that it adds namespaces less aggressively: I added a namespace only if there was not an explicit namespace after the initial "fluff". In counterexamples, I added namespaces to all files. I introduced three "main" namespaces: imo, theorems_100, counterexample (the last one singular). Besides these, I also introduced the namespaces prop_encodable, oxford_invariants, sensitivity, to cover the left-over files in archive. Note that if a file has namespace early on, then it does not get a new namespace, even though it might be desirable for it to have one. Comments are very welcome! Note: besides adding namespaces, the only files that I had to manually edit are the ones in

• commit d337b99e3e6d147d440c91874d1809a3ee04ff16 -- I do not like these changes, but currently do not see how to avoid them;
• commit 48471f35ec9f9929dd35363ee176f8c889042f6e -- I removed an pre-existing namespace, replacing it by open <itself>. Zulip discussion: this PR is motivated by the desire to port to mathlib4 the files in archive, counterexamples, taking advantage of mathport. The namespacing helps with avoiding clashes among names of declarations, as well as one-lettered declarations in the root namespace.