Definition df-hl 9730

Description: Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space.

Assertion

Ref	Expression
df-hl	|- CHil = (CBan i^i CPreHil)

Detailed syntax breakdown of Definition df-hl

Step	Hyp	Ref	Expression
1		chl 9729	. 2 class CHil
2		cbn 9659	. . 3 class CBan
3		cphl 9607	. . 3 class CPreHil
4	2, 3	cin 2425	. 2 class (CBan i^i CPreHil)
5	1, 4	wceq 1136	1 wff CHil = (CBan i^i CPreHil)

This definition is referenced by:  ishl 9731

Copyright terms: Public domain