mathlib

32837559 - chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129)

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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mk_all.2Esh): 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.