Нормированное векторное пространство

Нормированное векторное пространство над линейно упорядоченным полем

• $a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q$ - множества,
• $f = \mathrm{\Sigma}(g,h,i)$ - сигнатура,
• $\left|\circ \right|\in h\ \land \ i(\left|\circ \right|)=1_{\omega }$ - символ унарной операции,
• $j\in h\ \land \ i(j)=2_{\omega }\ \land \ k\in h\ \land \ i(k)=2_{\omega }$ - символы бинарных операций,
• $l\in g\ \land \ i(l)=2_{\omega }$ - символ бинарного отношения,
• $c = \mathrm{AlgStruct}(d,e,f)$ - алгебраическая структура,
• $c\in \mathrm{Field}(d;j,k)$ - поле,
• $c\in \mathrm{LinOrdStruct}(d;l)$ - линейно упорядоченная структура,
• $q = \left|\circ\right|_{j_c}^{l_c}$ - операция взятия модуля,
• $m\in \mathrm{Op}^2(b)$ - бинарная операция,
• $o=d\times b$ - прямое произведение,
• $n\in \mathrm{Function}(o,b)$ - функция,
• $p\in \mathrm {Function} (b,d)$ - функция.

Множество $a$ — нормированное векторное пространство (англ. normed vector space, нем. normierter Vektorraum) над полем $c$ или кратко нормированное векторное пространство, если выполняются следующие условия:

1. множество $a$ является упорядоченной пятёркой множеств $b,c,m,n,p$;
2. упорядоченная четвёрка множеств $\left\langle b,c,m,n\right\rangle$ является векторным пространством над полем $c$;
3. для любого элемента множества $b$ если значение функции $q$ от данного элемента множества $b$ равно некоторому нейтральному элементу интерпретации символа бинарной операции $j$, то данный элемент множества $b$ является нейтральным элементом бинарной операции $l$;
4. для любого элемента множества $b$ и для произвольного элемента множества $d$ значение функции $p$ от {значения функции $n$ от данного элемента множества $d$} и данного элемента множества $b$ равно значению интерпретации символа операции $k$ от модуля данного элемента множества $d$ и значения функции $n$ от данного элемента множества $b$;
5. для любых двух элементов множества $b$ упорядоченная пара {значения функции $q$ от {значения функции $m$ от первого элемента множества $b$ и второго элемента множества $b$}} и {значения интерпретации символа операции $j$ от {значения функции $q$ от первого элемента множества $b$} и {значения функции $q$ от второго элемента множества $b$}} принадлежит интерпретации символа отношения $l$:

$\Upsilon (a,\ldots ,q)\ {\stackrel {\mathrm {def} }{=}}\ {\begin{cases}a=\langle b,c,m,n,p\rangle \\\langle b,c,m,n\rangle =\mathrm {VectorSpace} (b,c;m,n)\\\forall r\quad r\in b\Rightarrow {\bigl (}\,(\exists s\quad s\in \mathrm {Neutral} (j_{c})\ \land \ s=p(r))\Rightarrow r\in \mathrm {Neutral} (m)\,{\bigr )}\\\forall r\ \forall s\quad (r\in b\ \land \ s\in d)\Rightarrow p(n(s,r))=k_{c}(q(s),p(r))\\\forall r\ \forall s\quad (r\in b\ \land \ s\in b)\Rightarrow {\bigl \langle }p{\bigl (}m(r,s){\bigr )},j_{c}{\bigl (}p(r),p(s){\bigr )}{\bigr \rangle }\in l_{c}\\\end{cases}}$

Обозначим $\Upsilon (a,\ldots ,q)\ {\stackrel {\mathrm {def} }{=}}\ a=\mathrm {NormedVectorSpace} (b,c;m,n,p)$.