Definition df-nm 8219

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 8209	. 2 class norm
2		c2nd 4078	. 2 class 2nd
3	1, 2	wceq 956	1 wff norm = 2nd

This definition is referenced by:  nmfval 8226

Copyright terms: Public domain