Definition df-hl 8456

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 8455	. 2 class CHil
2		cbn 8388	. . 3 class CBan
3		cphl 8337	. . 3 class CPreHil
4	2, 3	cin 2017	. 2 class (CBan i^i CPreHil)
5	1, 4	wceq 1099	1 wff CHil = (CBan i^i CPreHil)

This definition is referenced by:  ishl 8457

Copyright terms: Public domain