Definition df-rrv 34443

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 34442	. 2 class rRndVar
2		vp	. . 3 setvar 𝑝
3		cprb 34409	. . 3 class Prob
4	2	cv 1539	. . . . 5 class 𝑝
5	4	cdm 5685	. . . 4 class dom 𝑝
6		cbrsiga 34182	. . . 4 class 𝔅ℝ
7		cmbfm 34250	. . . 4 class MblFnM
8	5, 6, 7	co 7431	. . 3 class (dom 𝑝MblFnM𝔅ℝ)
9	2, 3, 8	cmpt 5225	. 2 class (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
10	1, 9	wceq 1540	1 wff rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))

This definition is referenced by:  rrvmbfm  34444