Add topological entropy.

[D-Thomine]

Add files on topological entropy, separated in 3 sets:

• Miscellaneous: files which should be added to various existing Mathlib files. 4 files, mostly on ENNReal/EReal numbers.
• Main files: definition and main properties of the topological entropy.
• Systems: entropies of various systems (unions, products, subsytems, full shift).

I will add a documentation file later on to explain various design decisions. For now, most information can be found in the header of BET.TopologicalEntropy.DynamicalCover

The implementation uses uniform spaces, so as to be naturally defined for compact spaces (instead of having a metric definition and then prove its topological invariance) and be more flexible. We define the entropy of subsets so as to avoid working with subtypes. Finally, the entropy is an extended real: it may take infinite values.

[mseri]

Wow, nice!

[mseri]

This is a lot of stuff. I am going to merge it as is, so that we can start opening issues for the TODOs and starting the necessary discussions

[mseri]

Thanks a lot