Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sigagen Structured version   Unicode version

Definition df-sigagen 26750
Description: Define the sigma algebra generated by a given collection of sets as the intersection of all sigma algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)
Assertion
Ref Expression
df-sigagen  |- sigaGen  =  ( x  e.  _V  |->  |^|
{ s  e.  (sigAlgebra ` 
U. x )  |  x  C_  s }
)
Distinct variable group:    x, s

Detailed syntax breakdown of Definition df-sigagen
StepHypRef Expression
1 csigagen 26749 . 2  class sigaGen
2 vx . . 3  setvar  x
3 cvv 3078 . . 3  class  _V
42cv 1369 . . . . . 6  class  x
5 vs . . . . . . 7  setvar  s
65cv 1369 . . . . . 6  class  s
74, 6wss 3439 . . . . 5  wff  x  C_  s
84cuni 4202 . . . . . 6  class  U. x
9 csiga 26718 . . . . . 6  class sigAlgebra
108, 9cfv 5529 . . . . 5  class  (sigAlgebra `  U. x )
117, 5, 10crab 2803 . . . 4  class  { s  e.  (sigAlgebra `  U. x )  |  x  C_  s }
1211cint 4239 . . 3  class  |^| { s  e.  (sigAlgebra `  U. x )  |  x  C_  s }
132, 3, 12cmpt 4461 . 2  class  ( x  e.  _V  |->  |^| { s  e.  (sigAlgebra `  U. x )  |  x  C_  s } )
141, 13wceq 1370 1  wff sigaGen  =  ( x  e.  _V  |->  |^|
{ s  e.  (sigAlgebra ` 
U. x )  |  x  C_  s }
)
Colors of variables: wff setvar class
This definition is referenced by:  sigagenval  26751  dmsigagen  26755  brsiga  26765
  Copyright terms: Public domain W3C validator