Definition df-nm 8183

Description: Define the norm function in a normed complex vector space.

Assertion

Ref	Expression
df-nm	|- norm = 2nd

Detailed syntax breakdown of Definition df-nm

Step	Hyp	Ref	Expression
1		cnm 8173	. 2 class norm
2		c2nd 4071	. 2 class 2nd
3	1, 2	wceq 955	1 wff norm = 2nd

This definition is referenced by:  nmfval 8190

Copyright terms: Public domain