Definition df-ch0 10550

Description: Define the zero for closed subspaces of Hilbert space. See h0elch 10552 for closure law.

Assertion

Ref	Expression
df-ch0	|- 0H = {0h}

Detailed syntax breakdown of Definition df-ch0

Step	Hyp	Ref	Expression
1		c0h 10228	. 2 class 0H
2		c0v 10215	. . 3 class 0h
3	2	csn 2868	. 2 class {0h}
4	1, 3	wceq 1136	1 wff 0H = {0h}

This definition is referenced by:  elch0 10551  h0elch 10552  sh0le 10789  spansn0 10889  df0op2 11107  ho01i 11183  hh0oi 11258  nmop0h 11345

Copyright terms: Public domain