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

Definition df-prob 30800
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 = {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}

Detailed syntax breakdown of Definition df-prob
StepHypRef Expression
1 cprb 30799 . 2 class Prob
2 vp . . . . . . . 8 setvar 𝑝
32cv 1631 . . . . . . 7 class 𝑝
43cdm 5266 . . . . . 6 class dom 𝑝
54cuni 4588 . . . . 5 class dom 𝑝
65, 3cfv 6049 . . . 4 class (𝑝 dom 𝑝)
7 c1 10149 . . . 4 class 1
86, 7wceq 1632 . . 3 wff (𝑝 dom 𝑝) = 1
9 cmeas 30588 . . . . 5 class measures
109crn 5267 . . . 4 class ran measures
1110cuni 4588 . . 3 class ran measures
128, 2, 11crab 3054 . 2 class {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
131, 12wceq 1632 1 wff Prob = {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
Colors of variables: wff setvar class
This definition is referenced by:  elprob  30801
  Copyright terms: Public domain W3C validator