Definition df-ch0

Description: Define the zero for closed subspaces of Hilbert space. See h0elch for closure law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0h	$$class{0}_{\mathscr{H}}$$
1		c0v	$$class{0}_{ℎ}$$
2	1	csn	$$class\left\{0_{ℎ}\right\}$$
3	0 2	wceq	$$wff{0}_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$