Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rrv Structured version   Visualization version   GIF version

Definition df-rrv 29632
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
StepHypRef Expression
1 crrv 29631 . 2 class rRndVar
2 vp . . 3 setvar 𝑝
3 cprb 29598 . . 3 class Prob
42cv 1473 . . . . 5 class 𝑝
54cdm 5024 . . . 4 class dom 𝑝
6 cbrsiga 29373 . . . 4 class 𝔅
7 cmbfm 29441 . . . 4 class MblFnM
85, 6, 7co 6523 . . 3 class (dom 𝑝MblFnM𝔅)
92, 3, 8cmpt 4633 . 2 class (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅))
101, 9wceq 1474 1 wff rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅))
Colors of variables: wff setvar class
This definition is referenced by:  rrvmbfm  29633
  Copyright terms: Public domain W3C validator