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

Definition df-brsiga 27793
Description: A Borel Algebra is defined as a sigma algebra generated by a topology. 'The' Borel sigma algebra here refers to the sigma algebra generated by the topology of open intervals on real numbers. The Borel algebra of a given topology  J is the sigma-algebra generated by 
J,  (sigaGen `  J
), so there is no need to introduce a special constant function for Borel sigma Algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
Assertion
Ref Expression
df-brsiga  |- 𝔅  =  (sigaGen `  ( topGen `
 ran  (,) )
)

Detailed syntax breakdown of Definition df-brsiga
StepHypRef Expression
1 cbrsiga 27792 . 2  class 𝔅
2 cioo 11525 . . . . 5  class  (,)
32crn 5000 . . . 4  class  ran  (,)
4 ctg 14689 . . . 4  class  topGen
53, 4cfv 5586 . . 3  class  ( topGen ` 
ran  (,) )
6 csigagen 27778 . . 3  class sigaGen
75, 6cfv 5586 . 2  class  (sigaGen `  ( topGen `
 ran  (,) )
)
81, 7wceq 1379 1  wff 𝔅  =  (sigaGen `  ( topGen `
 ran  (,) )
)
Colors of variables: wff setvar class
This definition is referenced by:  brsiga  27794  brsigarn  27795  unibrsiga  27797  elmbfmvol2  27878  dya2iocbrsiga  27886  dya2icobrsiga  27887  sxbrsiga  27901  rrvadd  28031  rrvmulc  28032  orrvcval4  28043  orrvcoel  28044  orrvccel  28045
  Copyright terms: Public domain W3C validator