WIP Manifolds

[siraben]

Tracking PR for #29. Targets the EuclideanSpaces branch because it needs to make use of facts about R^n.

Rough checklist/wishlist

• Atlases
• Smooth atlases
• Maximal atlases
• Chart transformations
• Smooth structures
• Smooth maps
• Diffeomorphisms
• Submanifolds
• Products and sums of manifolds
• Tangent space
• Cotangent space
• Derivations
• Regular values
• Inverse function theorem
• Rank theorem
• Immersions and embeddings

[Columbus240]

You could state facts like Hausdorff (Sphere n) or Hausdorff (EuclideanSpace n) as Lemmas/Corollaries whose proof ends in Admitted. This would simplify the code style (we wouldn’t need to repeat the proofs) and would make clearer what facts we still need to prove.
Adding comments what we need to show for each admit, as you did above, is very useful as reader. Thanks.

[Columbus240]

We should be able to prove that RTop is homeomorphic to EuclideanSpace 1. Combining this with a lemma that if A, B are homeomorphic, they are also homeomorphic, we should be able to get a proof of locally homeomorphic RTop (EuclideanSpace 1).

[Columbus240]

I took the liberty to give a more general result, relating global and local homeomorphisms and using it to change the proof of locally_homeomorphic_refl.
I think we could/should do the following:

• Fix the compilation errors found by the CI.
• Move the definition of restriction to ZornsLemma, if some more lemmas or theorems about it become relevant. Since it does not depend on a topology.
• Maybe look for a simpler or "better" proof of homeomorphism_restriction. The one I gave was hastily given. But it probably doesn’t matter much.
• For second-countability of EuclideanSpace n, maybe prove/use the fact that finite products of second-countable spaces are second-countable again. Since Sphere n is a subset of an EuclideanSpace n, we get second-countability as well.
• To prove that EuclideanSpace n and Sphere n are Hausdorff, we only need to recall that they are metric spaces and all metric spaces are Hausdorff.
• The proof that RTop and EuclideanSpace 1 could be finished. The second equality needs a nasty induction/inversion on a member of Vector. Maybe g has to be defined differently for it to work well, or there could be a more general statement hiding.