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	$$⊢{\mathrm{RndVar}}_{ℝ}=\left(p\in \mathrm{Prob}⟼\mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrv	$$class{\mathrm{RndVar}}_{ℝ}$$
1		vp	$$setvarp$$
2		cprb	$$class\mathrm{Prob}$$
3	1	cv	$$setvarp$$
4	3	cdm	$$class\mathrm{dom}p$$
5		cmbfm	$$class{\mathrm{MblFn}}_{\mu }$$
6		cbrsiga	$$class{𝔅}_{ℝ}$$
7	4 6 5	co	$$class\left(\mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
8	1 2 7	cmpt	$$class\left(p\in \mathrm{Prob}⟼\mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
9	0 8	wceq	$$wff{\mathrm{RndVar}}_{ℝ}=\left(p\in \mathrm{Prob}⟼\mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$