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 26734
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 26733 . 2  class 𝔅
2 cioo 11404 . . . . 5  class  (,)
32crn 4942 . . . 4  class  ran  (,)
4 ctg 14487 . . . 4  class  topGen
53, 4cfv 5519 . . 3  class  ( topGen ` 
ran  (,) )
6 csigagen 26719 . . 3  class sigaGen
75, 6cfv 5519 . 2  class  (sigaGen `  ( topGen `
 ran  (,) )
)
81, 7wceq 1370 1  wff 𝔅  =  (sigaGen `  ( topGen `
 ran  (,) )
)
Colors of variables: wff setvar class
This definition is referenced by:  brsiga  26735  brsigarn  26736  unibrsiga  26738  elmbfmvol2  26819  dya2iocbrsiga  26827  dya2icobrsiga  26828  sxbrsiga  26842  rrvadd  26972  rrvmulc  26973  orrvcval4  26984  orrvcoel  26985  orrvccel  26986
  Copyright terms: Public domain W3C validator