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 28734
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 28733 . 2  class Prob
2 vp . . . . . . . 8  setvar  p
32cv 1402 . . . . . . 7  class  p
43cdm 4940 . . . . . 6  class  dom  p
54cuni 4188 . . . . 5  class  U. dom  p
65, 3cfv 5523 . . . 4  class  ( p `
 U. dom  p
)
7 c1 9441 . . . 4  class  1
86, 7wceq 1403 . . 3  wff  ( p `
 U. dom  p
)  =  1
9 cmeas 28524 . . . . 5  class measures
109crn 4941 . . . 4  class  ran measures
1110cuni 4188 . . 3  class  U. ran measures
128, 2, 11crab 2755 . 2  class  { p  e.  U. ran measures  |  ( p `
 U. dom  p
)  =  1 }
131, 12wceq 1403 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  28735
  Copyright terms: Public domain W3C validator