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

Definition df-pointsN 28380
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 28373 . 2  class  Points
2 vk . . 3  set  k
3 cvv 2727 . . 3  class  _V
4 vq . . . . . . 7  set  q
54cv 1618 . . . . . 6  class  q
6 vp . . . . . . . 8  set  p
76cv 1618 . . . . . . 7  class  p
87csn 3544 . . . . . 6  class  { p }
95, 8wceq 1619 . . . . 5  wff  q  =  { p }
102cv 1618 . . . . . 6  class  k
11 catm 28142 . . . . . 6  class  Atoms
1210, 11cfv 4592 . . . . 5  class  ( Atoms `  k )
139, 6, 12wrex 2510 . . . 4  wff  E. p  e.  ( Atoms `  k )
q  =  { p }
1413, 4cab 2239 . . 3  class  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } }
152, 3, 14cmpt 3974 . 2  class  ( k  e.  _V  |->  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } } )
161, 15wceq 1619 1  wff  Points  =  ( k  e.  _V  |->  { q  |  E. p  e.  ( Atoms `  k )
q  =  { p } } )
Colors of variables: wff set class
This definition is referenced by:  pointsetN  28619
  Copyright terms: Public domain W3C validator