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 = ( 𝑝 ∈ Prob ↦ ( dom 𝑝 MblFnM 𝔅ℝ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrv	⊢ rRndVar
1		vp	⊢ 𝑝
2		cprb	⊢ Prob
3	1	cv	⊢ 𝑝
4	3	cdm	⊢ dom 𝑝
5		cmbfm	⊢ MblFnM
6		cbrsiga	⊢ 𝔅ℝ
7	4 6 5	co	⊢ ( dom 𝑝 MblFnM 𝔅ℝ )
8	1 2 7	cmpt	⊢ ( 𝑝 ∈ Prob ↦ ( dom 𝑝 MblFnM 𝔅ℝ ) )
9	0 8	wceq	⊢ rRndVar = ( 𝑝 ∈ Prob ↦ ( dom 𝑝 MblFnM 𝔅ℝ ) )