mathlib3

f3326db1 - feat(normed_space): second countability for linear maps (#4099)

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.