Normed vector types, infinite norm, norm equivalence thm, continuity …

[Tragicus]

Continuity of linear functions in finite dimension

Motivation for this change

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

[CohenCyril]

@mkerjean FYI

[affeldt-aist]

99d840c0404b054c2be4cfac217891a4064e7521 is just a linting commit

[affeldt-aist]

I was also wondering whether we should not try to extract the lemmas about bigmax (of non-negative terms using 0 as the default element) or try to use bigmax with {nonneg _} because I know of at least to other PRs that are using the same elements (to deal with mx_norm or with variations of functions).