Commit 2020-09-12 18:30 f3326db1

feat(normed_space): second countability for linear maps (#4099) From the sphere eversion project, various lemmas about continuous linear maps and a theorem: if E is finite dimensional and F is second countable then the space of continuous linear maps from E to F is second countable.