Definition df-rrv 31694

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

Detailed syntax breakdown of Definition df-rrv

Step	Hyp	Ref	Expression
1		crrv 31693	. 2 class rRndVar
2		vp	. . 3 setvar 𝑝
3		cprb 31660	. . 3 class Prob
4	2	cv 1532	. . . . 5 class 𝑝
5	4	cdm 5549	. . . 4 class dom 𝑝
6		cbrsiga 31435	. . . 4 class 𝔅ℝ
7		cmbfm 31503	. . . 4 class MblFnM
8	5, 6, 7	co 7150	. . 3 class (dom 𝑝MblFnM𝔅ℝ)
9	2, 3, 8	cmpt 5138	. 2 class (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
10	1, 9	wceq 1533	1 wff rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))

This definition is referenced by:  rrvmbfm  31695