![]() |
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 33179 | . 2 class 𝔅ℝ | |
2 | cioo 13324 | . . . . 5 class (,) | |
3 | 2 | crn 5678 | . . . 4 class ran (,) |
4 | ctg 17383 | . . . 4 class topGen | |
5 | 3, 4 | cfv 6544 | . . 3 class (topGen‘ran (,)) |
6 | csigagen 33136 | . . 3 class sigaGen | |
7 | 5, 6 | cfv 6544 | . 2 class (sigaGen‘(topGen‘ran (,))) |
8 | 1, 7 | wceq 1542 | 1 wff 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) |
Colors of variables: wff setvar class |
This definition is referenced by: brsiga 33181 brsigarn 33182 unibrsiga 33184 elmbfmvol2 33266 dya2iocbrsiga 33274 dya2icobrsiga 33275 sxbrsiga 33289 rrvadd 33451 rrvmulc 33452 orrvcval4 33463 orrvcoel 33464 orrvccel 33465 |
Copyright terms: Public domain | W3C validator |