Definition df-rrv

Description: In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016) (Revised by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Assertion	df-rrv	|- rRndVar = ( p e. Prob |-> ( dom p MblFnM BrSiga ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrv	|- rRndVar
1		vp	|- p
2		cprb	|- Prob
3	1	cv	|- p
4	3	cdm	|- dom p
5		cmbfm	|- MblFnM
6		cbrsiga	|- BrSiga
7	4 6 5	co	|- ( dom p MblFnM BrSiga )
8	1 2 7	cmpt	|- ( p e. Prob |-> ( dom p MblFnM BrSiga ) )
9	0 8	wceq	|- rRndVar = ( p e. Prob |-> ( dom p MblFnM BrSiga ) )