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

Definition df-brsiga 33932
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 𝐽 is the sigma-algebra generated by 𝐽, (sigaGen‘𝐽), 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 33931 . 2 class 𝔅
2 cioo 13359 . . . . 5 class (,)
32crn 5679 . . . 4 class ran (,)
4 ctg 17422 . . . 4 class topGen
53, 4cfv 6549 . . 3 class (topGen‘ran (,))
6 csigagen 33888 . . 3 class sigaGen
75, 6cfv 6549 . 2 class (sigaGen‘(topGen‘ran (,)))
81, 7wceq 1533 1 wff 𝔅 = (sigaGen‘(topGen‘ran (,)))
Colors of variables: wff setvar class
This definition is referenced by:  brsiga  33933  brsigarn  33934  unibrsiga  33936  elmbfmvol2  34018  dya2iocbrsiga  34026  dya2icobrsiga  34027  sxbrsiga  34041  rrvadd  34203  rrvmulc  34204  orrvcval4  34215  orrvcoel  34216  orrvccel  34217
  Copyright terms: Public domain W3C validator