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

Tragicus wants to merge 2 commits intomath-comp:mastermath-comp/analysis:masterfrom

Tragicus:linear_findim_continuousTragicus/analysis:linear_findim_continuousCopy head branch name to clipboard