Span from matrix columns

Stream: new members

[Aron Erben]

Hello, I'm doing some Linear Algebra work right now. I have two matrices X1 and X2 and I would like to get the column span of them as if they were concatenated together. I found submodule.span, but I'm struggling to turn both of the matrices into a set of vectors. How could I do that? Am I even going the right way? Thanks in advance! :)

[Anne Baanen]

matrix m n R is just an abbreviation for m → n → R, so you can use docs#set.range, the range of a function

[Anne Baanen]

More precisely, the columns of a matrix A would be set.range A.transpose

[Anne Baanen]

Or written another way, set.range (λ i, (λ j, A j i))

[Aron Erben]

Perfect, thank you so much, so #check set.range X₁ᵀ ∪ set.range X₂ᵀ should do it, right?

I was playing with fintype and finset. I was not aware it was this easy to turn a function into a set, kinda makes sense in retrospect though :)