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

Definition df-lhyp 30177
Description: Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-lhyp  |-  LHyp  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  x (  <o  `  k
) ( 1. `  k ) } )
Distinct variable group:    x, k

Detailed syntax breakdown of Definition df-lhyp
StepHypRef Expression
1 clh 30173 . 2  class  LHyp
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vx . . . . . 6  set  x
54cv 1622 . . . . 5  class  x
62cv 1622 . . . . . 6  class  k
7 cp1 14144 . . . . . 6  class  1.
86, 7cfv 5255 . . . . 5  class  ( 1.
`  k )
9 ccvr 29452 . . . . . 6  class  <o
106, 9cfv 5255 . . . . 5  class  (  <o  `  k )
115, 8, 10wbr 4023 . . . 4  wff  x ( 
<o  `  k ) ( 1. `  k )
12 cbs 13148 . . . . 5  class  Base
136, 12cfv 5255 . . . 4  class  ( Base `  k )
1411, 4, 13crab 2547 . . 3  class  { x  e.  ( Base `  k
)  |  x ( 
<o  `  k ) ( 1. `  k ) }
152, 3, 14cmpt 4077 . 2  class  ( k  e.  _V  |->  { x  e.  ( Base `  k
)  |  x ( 
<o  `  k ) ( 1. `  k ) } )
161, 15wceq 1623 1  wff  LHyp  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  x (  <o  `  k
) ( 1. `  k ) } )
Colors of variables: wff set class
This definition is referenced by:  lhpset  30184
  Copyright terms: Public domain W3C validator