Product of Euclidean spaces

Stream: Is there code for X?

[Michael Rothgang]

The following should be some fact about pi types (i.e., I would prove this first at that level, and then for PiLp): does mathlib really not have this yet?

def EuclideanSpace.prod (α β : Type*) :
    (EuclideanSpace ℝ α) × (EuclideanSpace ℝ β) ≃ EuclideanSpace ℝ (α ⊕ β) := sorry

(I'm interested in the corollary with α = Fin n and β = Fin m.)

[Floris van Doorn]

Isn't this docs#Equiv.sumArrowEquivProdArrow up to defeq? The Pi-version is docs#Equiv.sumPiEquivProdPi or docs#Equiv.prodPiEquivSumPi

[Floris van Doorn]

Found with

[Floris van Doorn]

@loogle Prod, Equiv, Sum

[loogle]

:search: Equiv.boolProdEquivSum, Equiv.sumArrowEquivProdArrow, and 61 more

[Floris van Doorn]

(it's not easy to search for Pi-types in Loogle, I think)

[Floris van Doorn]

docs#ContinuousLinearEquiv.sumPiEquivProdPi might also be relevant.

[Michael Rothgang]

Thanks, the first one did the trick!

[Eric Wieser]

I would guess you want WithLp on the LHS?

[Michael Rothgang]

I do in fact want a homeomorphism between these spaces, so I guess WithLp does help.

[Eric Wieser]

docs#LinearIsometryEquiv.piLpCurry may also be of interest

[Michael Rothgang]

I was just looking for that: this looks helpful, thanks!

[Eric Wieser]

Probably we should have LinearIsometryEquiv.sumPiLpEquivProdPiLp for the version you asked for

[Michael Rothgang]

That sounds exactly like what I need, indeed!

[Michael Rothgang]

Linking #22973 for posterity

[Eric Wieser]

Whoops, I'd forgotten that this is the second time this has been asked for

[Eric Wieser]

I've marked it "please adopt", since in the other thread about it I delegated filling the final two sorrys

[Jihoon Hyun]

The full proof has now been committed to #22973 !

[Eric Wieser]

The dependencies of that PR are now all resolved. Thanks for filling in the gaps, @Jihoon Hyun!