ChartedSpace of Euclid m and Euclid n with Euclid m+n

Stream: Is there code for X?

[Dominic Steinitz]

I couldn't find this or a theorem that gave me this

instance (m n : ℕ) : ChartedSpace ((EuclideanSpace ℝ (Fin (m + n)))) (EuclideanSpace ℝ (Fin m) × (EuclideanSpace ℝ (Fin n)))

[Michael Rothgang]

Good question! I'd prove this in two steps

• firstly, you can apply docs#PartialHomeomorph.singletonChartedSpace --- and reduce this question to finding a homeomorphism between those
• for that, see #Is there code for X? > Product of Euclidean spaces --- from there, you can get a continuous linear equivalence between Euclid (m+n) and Euclid m \times Euclid n, which is also a homeomorphism

[Michael Rothgang]

(And I personally think this continuous linear equivalence between Euclidean spaces specifically could be useful to add. Yes, you should usually not use it, but in examples you want to have it handy.)

[Dominic Steinitz]

Great - thanks very much - I am away on business next week - it may have to wait until the week after until I get a chance to try.