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 28834
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 28833 . 2  class 𝔅
2 cioo 11635 . . . . 5  class  (,)
32crn 4855 . . . 4  class  ran  (,)
4 ctg 15286 . . . 4  class  topGen
53, 4cfv 5601 . . 3  class  ( topGen ` 
ran  (,) )
6 csigagen 28790 . . 3  class sigaGen
75, 6cfv 5601 . 2  class  (sigaGen `  ( topGen `
 ran  (,) )
)
81, 7wceq 1437 1  wff 𝔅  =  (sigaGen `  ( topGen `
 ran  (,) )
)
Colors of variables: wff setvar class
This definition is referenced by:  brsiga  28835  brsigarn  28836  unibrsiga  28838  elmbfmvol2  28919  dya2iocbrsiga  28927  dya2icobrsiga  28928  sxbrsiga  28942  rrvadd  29102  rrvmulc  29103  orrvcval4  29114  orrvcoel  29115  orrvccel  29116
  Copyright terms: Public domain W3C validator