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 32371
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 32370 . 2 class Prob
2 vp . . . . . . . 8 setvar 𝑝
32cv 1541 . . . . . . 7 class 𝑝
43cdm 5590 . . . . . 6 class dom 𝑝
54cuni 4845 . . . . 5 class dom 𝑝
65, 3cfv 6432 . . . 4 class (𝑝 dom 𝑝)
7 c1 10873 . . . 4 class 1
86, 7wceq 1542 . . 3 wff (𝑝 dom 𝑝) = 1
9 cmeas 32159 . . . . 5 class measures
109crn 5591 . . . 4 class ran measures
1110cuni 4845 . . 3 class ran measures
128, 2, 11crab 3070 . 2 class {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
131, 12wceq 1542 1 wff Prob = {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
Colors of variables: wff setvar class
This definition is referenced by:  elprob  32372
  Copyright terms: Public domain W3C validator