normed type neighborhood lemmas - #2030

normed type neighborhood lemmas#2030

amolinamounier wants to merge 8 commits into

math-comp:mastermath-comp/analysis:masterfrom

amolinamounier:normed_nbhs_lemmasamolinamounier/mathcomp-analysis:normed_nbhs_lemmasCopy head branch name to clipboard