Linear_continuous structure

[mkerjean]

Motivation for this change

This PR gives the structure of a lmdotype R to:

• {linear E -> F} when E, F : lmodType R
• {linear_continuous E -> F} when E F : convextvsType R. It also defined the {linear_continuous _ -> _} structure.

This development is essential to the study of topological duals E' in topological vector spaces, and more generally to the study of closed categories in functional analysis.
Another pull request will enforce the topological structures on {linear_continuous E -> F} ( as a convextvsType, or metric/normed when F is metric or normed).

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@CohenCyril could you take a quick look at this PR?
We have been testing it with the Hahn-Banach proof, so it should be mostly ok.

However, we have observed one thing that we would like to address later:
pseudometric_normedZmodType is a morally a topologicalNmodule
but topologicalNmodule is defined later in tvs.v (which imports pseudometric_normed_zmodule.v).
We think that it should be defined at the beginning of pseudometric_normed_zmodule.v and that
pseudometric_normedZmodType should be defined using topologicalNmodule.
We have realized this because of the lemmas such as cvgD/fun_cvgD that we needed to duplicate.
We think that we can make this change and factorize lemmas but we would like to do it in a later PR.
We'll issue about this in the event this PR is merged.