Definition df-rrv 32408

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 32407	. 2 class rRndVar
2		vp	. . 3 setvar 𝑝
3		cprb 32374	. . 3 class Prob
4	2	cv 1538	. . . . 5 class 𝑝
5	4	cdm 5589	. . . 4 class dom 𝑝
6		cbrsiga 32149	. . . 4 class 𝔅ℝ
7		cmbfm 32217	. . . 4 class MblFnM
8	5, 6, 7	co 7275	. . 3 class (dom 𝑝MblFnM𝔅ℝ)
9	2, 3, 8	cmpt 5157	. 2 class (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
10	1, 9	wceq 1539	1 wff rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))

This definition is referenced by:  rrvmbfm  32409