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 31740
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 31739 . 2 class Prob
2 vp . . . . . . . 8 setvar 𝑝
32cv 1537 . . . . . . 7 class 𝑝
43cdm 5532 . . . . . 6 class dom 𝑝
54cuni 4813 . . . . 5 class dom 𝑝
65, 3cfv 6334 . . . 4 class (𝑝 dom 𝑝)
7 c1 10527 . . . 4 class 1
86, 7wceq 1538 . . 3 wff (𝑝 dom 𝑝) = 1
9 cmeas 31528 . . . . 5 class measures
109crn 5533 . . . 4 class ran measures
1110cuni 4813 . . 3 class ran measures
128, 2, 11crab 3134 . 2 class {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
131, 12wceq 1538 1 wff Prob = {𝑝 ran measures ∣ (𝑝 dom 𝑝) = 1}
Colors of variables: wff setvar class
This definition is referenced by:  elprob  31741
  Copyright terms: Public domain W3C validator