The differentiable functions from a proper closed interval of real numbers to a normed real vector space form a vector space#1980

lowasser wants to merge 4 commits into

UniMath:masterUniMath/agda-unimath:masterfrom

lowasser:vec-space-differentiable-functional-analysislowasser/agda-unimath:vec-space-differentiable-functional-analysisCopy head branch name to clipboard