Definition df-rrv 30503

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.)

Assertion

Ref	Expression
df-rrv	|- rRndVar = ( p e. Prob |-> ( dom pMblFnM𝔅ℝ ) )

Detailed syntax breakdown of Definition df-rrv

Step	Hyp	Ref	Expression
1		crrv 30502	. 2 class rRndVar
2		vp	. . 3 setvar p
3		cprb 30469	. . 3 class Prob
4	2	cv 1482	. . . . 5 class p
5	4	cdm 5114	. . . 4 class dom p
6		cbrsiga 30244	. . . 4 class 𝔅ℝ
7		cmbfm 30312	. . . 4 class MblFnM
8	5, 6, 7	co 6650	. . 3 class ( dom pMblFnM𝔅ℝ )
9	2, 3, 8	cmpt 4729	. 2 class ( p e. Prob |-> ( dom pMblFnM𝔅ℝ ) )
10	1, 9	wceq 1483	1 wff rRndVar = ( p e. Prob |-> ( dom pMblFnM𝔅ℝ ) )

This definition is referenced by:  rrvmbfm  30504