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

Definition df-rrv 26969
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  =  ( p  e. Prob  |->  ( dom  pMblFnM𝔅 ) )

Detailed syntax breakdown of Definition df-rrv
StepHypRef Expression
1 crrv 26968 . 2  class rRndVar
2 vp . . 3  setvar  p
3 cprb 26935 . . 3  class Prob
42cv 1369 . . . . 5  class  p
54cdm 4949 . . . 4  class  dom  p
6 cbrsiga 26741 . . . 4  class 𝔅
7 cmbfm 26810 . . . 4  class MblFnM
85, 6, 7co 6201 . . 3  class  ( dom  pMblFnM𝔅 )
92, 3, 8cmpt 4459 . 2  class  ( p  e. Prob  |->  ( dom  pMblFnM𝔅 ) )
101, 9wceq 1370 1  wff rRndVar  =  ( p  e. Prob  |->  ( dom  pMblFnM𝔅 ) )
Colors of variables: wff setvar class
This definition is referenced by:  rrvmbfm  26970
  Copyright terms: Public domain W3C validator