Definition df-hl 8547

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 8546	. 2 class CHil
2		cbn 8479	. . 3 class CBan
3		cphl 8428	. . 3 class CPreHil
4	2, 3	cin 2044	. 2 class (CBan i^i CPreHil)
5	1, 4	wceq 956	1 wff CHil = (CBan i^i CPreHil)

This definition is referenced by:  ishl 8548

Copyright terms: Public domain