Definition df-ch0 9080

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

Assertion

Ref	Expression
df-ch0	⊢ 0ℋ = {0h}

Detailed syntax breakdown of Definition df-ch0

Step	Hyp	Ref	Expression
1		c0h 8759	. 2 class 0ℋ
2		c0v 8746	. . 3 class 0h
3	2	csn 2406	. 2 class {0h}
4	1, 3	wceq 955	1 wff 0ℋ = {0h}

This definition is referenced by:  elch0 9081  h0elch 9082  sh0let 9319  spansn0 9419  df0op2 9635  ho01 9711  hh0o 9786  nmop0h 9872

Copyright terms: Public domain