How to concatenate vectors in Euclidean spaces

Stream: new members

[Giovanni Mascellani]

Given x : euclidean_space k n and y : euclidean_space k m, is there a definition already of the concatenation of x and y as an element of euclidean_space k (n + m)? Browsing the mathlib docs I couldn't find anything, but it seems a general concept enough that it should have a place there.

[Eric Wieser]

This doesn't exist, but the pieces to form it do

[Eric Wieser]

Something like (pi_Lp.equiv _ _).symm (sum.elim (pi_Lp.equiv _ _ x) (pi_Lp.equiv _ _ y))