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 30444
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 30443 . 2 class Prob
2 vp . . . . . . . 8 setvar 𝑝
32cv 1480 . . . . . . 7 class 𝑝
43cdm 5104 . . . . . 6 class dom 𝑝
54cuni 4427 . . . . 5 class dom 𝑝
65, 3cfv 5876 . . . 4 class (𝑝 dom 𝑝)
7 c1 9922 . . . 4 class 1
86, 7wceq 1481 . . 3 wff (𝑝 dom 𝑝) = 1
9 cmeas 30232 . . . . 5 class measures
109crn 5105 . . . 4 class ran measures
1110cuni 4427 . . 3 class ran measures
128, 2, 11crab 2913 . 2 class {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
131, 12wceq 1481 1 wff Prob = {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
Colors of variables: wff setvar class
This definition is referenced by:  elprob  30445
  Copyright terms: Public domain W3C validator