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

Definition df-pclN 29207
Description: Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in  PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces  PSubCl of df-psubclN 29254.) (Contributed by NM, 7-Sep-2013.)
Assertion
Ref Expression
df-pclN  |-  PCl  =  ( k  e.  _V  |->  ( x  e.  ~P ( Atoms `  k )  |-> 
|^| { y  e.  (
PSubSp `  k )  |  x  C_  y }
) )
Distinct variable group:    x, k, y

Detailed syntax breakdown of Definition df-pclN
StepHypRef Expression
1 cpclN 29206 . 2  class  PCl
2 vk . . 3  set  k
3 cvv 2740 . . 3  class  _V
4 vx . . . 4  set  x
52cv 1618 . . . . . 6  class  k
6 catm 28583 . . . . . 6  class  Atoms
75, 6cfv 4638 . . . . 5  class  ( Atoms `  k )
87cpw 3566 . . . 4  class  ~P ( Atoms `  k )
94cv 1618 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1618 . . . . . . 7  class  y
129, 11wss 3094 . . . . . 6  wff  x  C_  y
13 cpsubsp 28815 . . . . . . 7  class  PSubSp
145, 13cfv 4638 . . . . . 6  class  ( PSubSp `  k )
1512, 10, 14crab 2519 . . . . 5  class  { y  e.  ( PSubSp `  k
)  |  x  C_  y }
1615cint 3803 . . . 4  class  |^| { y  e.  ( PSubSp `  k
)  |  x  C_  y }
174, 8, 16cmpt 4017 . . 3  class  ( x  e.  ~P ( Atoms `  k )  |->  |^| { y  e.  ( PSubSp `  k
)  |  x  C_  y } )
182, 3, 17cmpt 4017 . 2  class  ( k  e.  _V  |->  ( x  e.  ~P ( Atoms `  k )  |->  |^| { y  e.  ( PSubSp `  k
)  |  x  C_  y } ) )
191, 18wceq 1619 1  wff  PCl  =  ( k  e.  _V  |->  ( x  e.  ~P ( Atoms `  k )  |-> 
|^| { y  e.  (
PSubSp `  k )  |  x  C_  y }
) )
Colors of variables: wff set class
This definition is referenced by:  pclfvalN  29208
  Copyright terms: Public domain W3C validator