Definition df-hl 8534

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 ∩ CPreHil)

Detailed syntax breakdown of Definition df-hl

Step	Hyp	Ref	Expression
1		chl 8533	. 2 class CHil
2		cbn 8466	. . 3 class CBan
3		cphl 8415	. . 3 class CPreHil
4	2, 3	cin 2042	. 2 class (CBan ∩ CPreHil)
5	1, 4	wceq 954	1 wff CHil = (CBan ∩ CPreHil)

This definition is referenced by:  ishl 8535

Copyright terms: Public domain