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

Definition df-prob 26955
Description: Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.)
Assertion
Ref Expression
df-prob  |- Prob  =  {
p  e.  U. ran measures  |  ( p `  U. dom  p )  =  1 }

Detailed syntax breakdown of Definition df-prob
StepHypRef Expression
1 cprb 26954 . 2  class Prob
2 vp . . . . . . . 8  setvar  p
32cv 1369 . . . . . . 7  class  p
43cdm 4951 . . . . . 6  class  dom  p
54cuni 4202 . . . . 5  class  U. dom  p
65, 3cfv 5529 . . . 4  class  ( p `
 U. dom  p
)
7 c1 9397 . . . 4  class  1
86, 7wceq 1370 . . 3  wff  ( p `
 U. dom  p
)  =  1
9 cmeas 26774 . . . . 5  class measures
109crn 4952 . . . 4  class  ran measures
1110cuni 4202 . . 3  class  U. ran measures
128, 2, 11crab 2803 . 2  class  { p  e.  U. ran measures  |  ( p `
 U. dom  p
)  =  1 }
131, 12wceq 1370 1  wff Prob  =  {
p  e.  U. ran measures  |  ( p `  U. dom  p )  =  1 }
Colors of variables: wff setvar class
This definition is referenced by:  elprob  26956
  Copyright terms: Public domain W3C validator