Definition df-brsiga

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 J is the sigma-algebra generated by J , ( sigaGenJ ) , so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	df-brsiga	|- BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbrsiga	|- BrSiga
1		csigagen	|- sigaGen
2		ctg	|- topGen
3		cioo	|- (,)
4	3	crn	|- ran (,)
5	4 2	cfv	|- ( topGen ` ran (,) )
6	5 1	cfv	|- ( sigaGen ` ( topGen ` ran (,) ) )
7	0 6	wceq	|- BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )