| 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 34182 | . 2 class 𝔅ℝ | |
| 2 | cioo 13387 | . . . . 5 class (,) | |
| 3 | 2 | crn 5686 | . . . 4 class ran (,) |
| 4 | ctg 17482 | . . . 4 class topGen | |
| 5 | 3, 4 | cfv 6561 | . . 3 class (topGen‘ran (,)) |
| 6 | csigagen 34139 | . . 3 class sigaGen | |
| 7 | 5, 6 | cfv 6561 | . 2 class (sigaGen‘(topGen‘ran (,))) |
| 8 | 1, 7 | wceq 1540 | 1 wff 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) |
| Colors of variables: wff setvar class |
| This definition is referenced by: brsiga 34184 brsigarn 34185 unibrsiga 34187 elmbfmvol2 34269 dya2iocbrsiga 34277 dya2icobrsiga 34278 sxbrsiga 34292 rrvadd 34454 rrvmulc 34455 orrvcval4 34467 orrvcoel 34468 orrvccel 34469 |
| Copyright terms: Public domain | W3C validator |