[Merged by Bors] - feat(normed_space): second countability for linear maps

[PatrickMassot]

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.

---

[sgouezel]

Looks good to me, thanks!

A possibility to factor a useful lemma out of the proof of the instance, to streamline it even a little bit more (although I already like how the proof looks!):

Given a basis on a finite-dimensional space, there exists a positive constant C such that, if two continuous linear maps satisfy u e - v e \leq M for all e in the basis, then ||u - v|| \leq C M.

[sgouezel]

Given a basis on a finite-dimensional space, there exists a positive constant C such that, if two continuous linear maps satisfy u e - v e \leq M for all e in the basis, then ||u - v|| \leq C M.

Better: do that only with one function: if ||u e|| \leq M for all e in the basis, then ||u|| \leq C M.

(Then this can be applied to u - v when needed)

[sgouezel]

I feel this lemma should be proved for the algebraic version (i.e., hv.constr without the L), probably with a simp attribute, and then the lemma for hv.constrL should follow (directly or by simp). Same thing for the next lemma.

[PatrickMassot]

The situation is more complicated because hv.constr makes sense also in infinite dimension so everything is somehow duplicated, with lemmas about functions vs lemmas about finitely supported functions. But of course in this file I assume the source has finite dimension. So I added a finite dimensional version on the algebraic side.

[sgouezel]

In a conversation (in which I can't currently answer, I don't know why), you say:

The last part of your second sentence is unfortunately not true. I tried switching to you version but (hv.constrL $ u ∘ n) (v i) no longer simplify nicely, even when I also transformed the statement of is_basis.constrL_apply_self.

If I understand correctly what is going on, the problem is that the simplifier becomes more powerful with my version of the lemma, therefore it simplifies the function application earlier, and you end up with a different simp normal form, that the simplifier does not simplify more because it doesn't have the relevant simp lemmas. Does it mean that we are missing some simp lemmas here?

[PatrickMassot]

In a conversation (in which I can't currently answer, I don't know why), you say:

The last part of your second sentence is unfortunately not true. I tried switching to you version but (hv.constrL $ u ∘ n) (v i) no longer simplify nicely, even when I also transformed the statement of is_basis.constrL_apply_self.

If I understand correctly what is going on, the problem is that the simplifier becomes more powerful with my version of the lemma, therefore it simplifies the function application earlier, and you end up with a different simp normal form, that the simplifier does not simplify more because it doesn't have the relevant simp lemmas. Does it mean that we are missing some simp lemmas here?

My memory is that the situation was more complicated than that, but now I can't even make it a simp lemma in your form, Lean complains this is not a valid simp lemma.

[sgouezel]

My memory is that the situation was more complicated than that, but now I can't even make it a simp lemma in your form, Lean complains this is not a valid simp lemma.

ok, let's ignore this, and we'll change it if the need shows up later. You can merge this once the linter is happy.

bors d+

[bors]

✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[PatrickMassot]

Thanks for all you comments!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests