Definition df-hl 8850

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 8849	. 2 class CHil
2		cbn 8779	. . 3 class CBan
3		cphl 8727	. . 3 class CPreHil
4	2, 3	cin 2098	. 2 class (CBan i^i CPreHil)
5	1, 4	wceq 992	1 wff CHil = (CBan i^i CPreHil)

This definition is referenced by:  ishl 8851

Copyright terms: Public domain