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

Definition df-pointsN 33454
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  |-  Points  =  ( k  e.  _V  |->  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } } )
Distinct variable group:    k, p, q

Detailed syntax breakdown of Definition df-pointsN
StepHypRef Expression
1 cpointsN 33447 . 2  class  Points
2 vk . . 3  setvar  k
3 cvv 3070 . . 3  class  _V
4 vq . . . . . . 7  setvar  q
54cv 1369 . . . . . 6  class  q
6 vp . . . . . . . 8  setvar  p
76cv 1369 . . . . . . 7  class  p
87csn 3977 . . . . . 6  class  { p }
95, 8wceq 1370 . . . . 5  wff  q  =  { p }
102cv 1369 . . . . . 6  class  k
11 catm 33216 . . . . . 6  class  Atoms
1210, 11cfv 5518 . . . . 5  class  ( Atoms `  k )
139, 6, 12wrex 2796 . . . 4  wff  E. p  e.  ( Atoms `  k )
q  =  { p }
1413, 4cab 2436 . . 3  class  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } }
152, 3, 14cmpt 4450 . 2  class  ( k  e.  _V  |->  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } } )
161, 15wceq 1370 1  wff  Points  =  ( k  e.  _V  |->  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } } )
Colors of variables: wff setvar class
This definition is referenced by:  pointsetN  33693
  Copyright terms: Public domain W3C validator