Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pointsN Unicode version

Definition df-pointsN 29632
 Description: Define set of all projective points in a Hilbert lattice (actually in any set at all, for simplicity). A projective point is the singleton of a lattice atom. Definition 15.1 of [MaedaMaeda] p. 61. Note that item 1 in [Holland95] p. 222 defines a point as the atom itself, but this leads to a complicated subspace ordering that may be either membership or inclusion based on its arguments. (Contributed by NM, 2-Oct-2011.)
Assertion
Ref Expression
df-pointsN
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-pointsN
StepHypRef Expression
1 cpointsN 29625 . 2
2 vk . . 3
3 cvv 2913 . . 3
4 vq . . . . . . 7
54cv 1648 . . . . . 6
6 vp . . . . . . . 8
76cv 1648 . . . . . . 7
87csn 3771 . . . . . 6
95, 8wceq 1649 . . . . 5
102cv 1648 . . . . . 6
11 catm 29394 . . . . . 6
1210, 11cfv 5408 . . . . 5
139, 6, 12wrex 2664 . . . 4
1413, 4cab 2387 . . 3
152, 3, 14cmpt 4221 . 2
161, 15wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  pointsetN  29871
 Copyright terms: Public domain W3C validator