Description: Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-nghm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cnghm | |
|
1 | vs | |
|
2 | cngp | |
|
3 | vt | |
|
4 | 1 | cv | |
5 | cnmo | |
|
6 | 3 | cv | |
7 | 4 6 5 | co | |
8 | 7 | ccnv | |
9 | cr | |
|
10 | 8 9 | cima | |
11 | 1 3 2 2 10 | cmpo | |
12 | 0 11 | wceq | |