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

Definition df-llines 29687
Description: Define the set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice  k, in other words all elements of height 2 (or lattice dimension 2 or projective dimension 1). (Contributed by NM, 16-Jun-2012.)
Assertion
Ref Expression
df-llines  |-  LLines  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  E. p  e.  ( Atoms `  k ) p ( 
<o  `  k ) x } )
Distinct variable group:    k, p, x

Detailed syntax breakdown of Definition df-llines
StepHypRef Expression
1 clln 29680 . 2  class  LLines
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vp . . . . . . 7  set  p
54cv 1622 . . . . . 6  class  p
6 vx . . . . . . 7  set  x
76cv 1622 . . . . . 6  class  x
82cv 1622 . . . . . . 7  class  k
9 ccvr 29452 . . . . . . 7  class  <o
108, 9cfv 5255 . . . . . 6  class  (  <o  `  k )
115, 7, 10wbr 4023 . . . . 5  wff  p ( 
<o  `  k ) x
12 catm 29453 . . . . . 6  class  Atoms
138, 12cfv 5255 . . . . 5  class  ( Atoms `  k )
1411, 4, 13wrex 2544 . . . 4  wff  E. p  e.  ( Atoms `  k )
p (  <o  `  k
) x
15 cbs 13148 . . . . 5  class  Base
168, 15cfv 5255 . . . 4  class  ( Base `  k )
1714, 6, 16crab 2547 . . 3  class  { x  e.  ( Base `  k
)  |  E. p  e.  ( Atoms `  k )
p (  <o  `  k
) x }
182, 3, 17cmpt 4077 . 2  class  ( k  e.  _V  |->  { x  e.  ( Base `  k
)  |  E. p  e.  ( Atoms `  k )
p (  <o  `  k
) x } )
191, 18wceq 1623 1  wff  LLines  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  E. p  e.  ( Atoms `  k ) p ( 
<o  `  k ) x } )
Colors of variables: wff set class
This definition is referenced by:  llnset  29694
  Copyright terms: Public domain W3C validator