Commit 2020-05-01 05:59 74d24aba
View on Github →feat(topology/instances/real_vector_space): E →+ F to E →L[ℝ] F (#2577)
A continuous additive map between two vector spaces over ℝ is ℝ-linear.
feat(topology/instances/real_vector_space): E →+ F to E →L[ℝ] F (#2577)
A continuous additive map between two vector spaces over ℝ is ℝ-linear.