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 31435 | . 2 class 𝔅ℝ | |
2 | cioo 12732 | . . . . 5 class (,) | |
3 | 2 | crn 5550 | . . . 4 class ran (,) |
4 | ctg 16705 | . . . 4 class topGen | |
5 | 3, 4 | cfv 6349 | . . 3 class (topGen‘ran (,)) |
6 | csigagen 31392 | . . 3 class sigaGen | |
7 | 5, 6 | cfv 6349 | . 2 class (sigaGen‘(topGen‘ran (,))) |
8 | 1, 7 | wceq 1533 | 1 wff 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) |
Colors of variables: wff setvar class |
This definition is referenced by: brsiga 31437 brsigarn 31438 unibrsiga 31440 elmbfmvol2 31520 dya2iocbrsiga 31528 dya2icobrsiga 31529 sxbrsiga 31543 rrvadd 31705 rrvmulc 31706 orrvcval4 31717 orrvcoel 31718 orrvccel 31719 |
Copyright terms: Public domain | W3C validator |