Random projection on subspace

Stream: new members

[Nicolò Cavalleri]

I have a normed vector space E and a subspace S and I want to write a "random" (not in any probabilistic sense) projection from E to S. I don't have that my space is complete nor that the field is R or C but I actually do not care that the projection has anything to do with the orthogonal projection, any projection is ok. What is the easiest way to do that?

[Kyle Miller]

Are you wanting a projection as a hypothesis, or do you want to show one exists?

[Anatole Dedecker]

I would use docs#submodule.exists_is_compl

[Anatole Dedecker]

And docs#submodule.linear_proj_of_is_compl