Definition df-rrv 29830

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 29829	. 2 class rRndVar
2		vp	. . 3 setvar 𝑝
3		cprb 29796	. . 3 class Prob
4	2	cv 1474	. . . . 5 class 𝑝
5	4	cdm 5038	. . . 4 class dom 𝑝
6		cbrsiga 29571	. . . 4 class 𝔅ℝ
7		cmbfm 29639	. . . 4 class MblFnM
8	5, 6, 7	co 6549	. . 3 class (dom 𝑝MblFnM𝔅ℝ)
9	2, 3, 8	cmpt 4643	. 2 class (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
10	1, 9	wceq 1475	1 wff rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))

This definition is referenced by:  rrvmbfm  29831