HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-sh Unicode version

Definition df-sh 22745
Description: Define the set of subspaces of a Hilbert space. See issh 22746 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-sh

Detailed syntax breakdown of Definition df-sh
StepHypRef Expression
1 csh 22467 . 2
2 c0v 22463 . . . . 5
3 vh . . . . . 6
43cv 1653 . . . . 5
52, 4wcel 1728 . . . 4
6 cva 22459 . . . . . 6
74, 4cxp 4921 . . . . . 6
86, 7cima 4926 . . . . 5
98, 4wss 3313 . . . 4
10 csm 22460 . . . . . 6
11 cc 9043 . . . . . . 7
1211, 4cxp 4921 . . . . . 6
1310, 12cima 4926 . . . . 5
1413, 4wss 3313 . . . 4
155, 9, 14w3a 937 . . 3
16 chil 22458 . . . 4
1716cpw 3830 . . 3
1815, 3, 17crab 2720 . 2
191, 18wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  issh  22746
  Copyright terms: Public domain W3C validator