Definition df-nm 9551

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 9541	. 2 class norm
2		c2nd 5019	. 2 class 2nd
3	1, 2	wceq 1298	1 wff norm = 2nd

This definition is referenced by:  nmfval 9558

Copyright terms: Public domain