Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nghm Structured version   Unicode version

Definition df-nghm 18743
 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.)
Assertion
Ref Expression
df-nghm NGHom NrmGrp NrmGrp
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-nghm
StepHypRef Expression
1 cnghm 18740 . 2 NGHom
2 vs . . 3
3 vt . . 3
4 cngp 18625 . . 3 NrmGrp
52cv 1651 . . . . . 6
63cv 1651 . . . . . 6
7 cnmo 18739 . . . . . 6
85, 6, 7co 6081 . . . . 5
98ccnv 4877 . . . 4
10 cr 8989 . . . 4
119, 10cima 4881 . . 3
122, 3, 4, 4, 11cmpt2 6083 . 2 NrmGrp NrmGrp
131, 12wceq 1652 1 NGHom NrmGrp NrmGrp
 Colors of variables: wff set class This definition is referenced by:  reldmnghm  18746  nghmfval  18756
 Copyright terms: Public domain W3C validator