![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-brsiga | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-brsiga | ⊢ 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbrsiga 34162 | . 2 class 𝔅ℝ | |
2 | cioo 13384 | . . . . 5 class (,) | |
3 | 2 | crn 5690 | . . . 4 class ran (,) |
4 | ctg 17484 | . . . 4 class topGen | |
5 | 3, 4 | cfv 6563 | . . 3 class (topGen‘ran (,)) |
6 | csigagen 34119 | . . 3 class sigaGen | |
7 | 5, 6 | cfv 6563 | . 2 class (sigaGen‘(topGen‘ran (,))) |
8 | 1, 7 | wceq 1537 | 1 wff 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) |
Colors of variables: wff setvar class |
This definition is referenced by: brsiga 34164 brsigarn 34165 unibrsiga 34167 elmbfmvol2 34249 dya2iocbrsiga 34257 dya2icobrsiga 34258 sxbrsiga 34272 rrvadd 34434 rrvmulc 34435 orrvcval4 34446 orrvcoel 34447 orrvccel 34448 |
Copyright terms: Public domain | W3C validator |