definition of norm on real or complex vectors space, induced by 'vectors spaces - linear morphisms' isomorphism
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of norm on real or complex vectors space.
- The reader knows a definition of %category name% isomorphism.
Target Context
- The reader will have a definition of norm on real or complex vectors space, induced by 'vectors spaces - linear morphisms' isomorphism.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\( F\): \(\in \{\mathbb{R}, \mathbb{C}\}\), with the canonical field structure
\( V\): \(\in \{\text{ the } F \text{ vectors spaces }\}\)
\( V'\): \(\in \{\text{ the } F \text{ vectors spaces }\}\)
\( \Vert \bullet \Vert'\): \(: V' \to \mathbb{R}\), \(\in \{\text{ the norms on } V'\}\)
\( f\): \(: V \to V'\), \(\in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
\(*\Vert \bullet \Vert\): \(: V \to \mathbb{R}, v \mapsto \Vert f (v) \Vert'\), \(\in \{\text{ the norms on } V\}\)
//
Conditions:
//
2: Note
Let us see that \(\Vert \bullet \Vert\) is indeed a norm on \(V\).
Let \(v_1, v_2 \in V\) and \(r \in F\) be any.
1) (\(0 \le \Vert v_1 \Vert\)) \(\land\) (\((0 = \Vert v_1 \Vert) \iff (v_1 = 0)\)): \(0 \le \Vert f (v_1) \Vert' = \Vert v_1 \Vert\); if \(v_1 = 0\), \(f (v_1) = 0\), so, \(\Vert v_1 \Vert = \Vert f (v_1) \Vert' = 0\), while if \(\Vert v_1 \Vert = \Vert f (v_1) \Vert' = 0\), \(f (v_1) = 0\), so, \(v_1 = 0\).
2) \(\Vert r v_1 \Vert = \vert r \vert \Vert v_1 \Vert\): \(\Vert r v_1 \Vert = \Vert f (r v_1) \Vert' = \Vert r f (v_1) \Vert' = \vert r \vert \Vert f (v_1) \Vert' = \vert r \vert \Vert v_1 \Vert\).
3) \(\Vert v_1 + v_2 \Vert \le \Vert v_1 \Vert + \Vert v_2 \Vert\): \(\Vert v_1 + v_2 \Vert = \Vert f (v_1 + v_2) \Vert' = \Vert f (v_1) + f (v_2) \Vert' \le \Vert f (v_1) \Vert' + \Vert f (v_2) \Vert' = \Vert v_1 \Vert + \Vert v_2 \Vert\).
