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

Definition df-orvc 28659
Description: Define the preimage set mapping operator. In probability theory, the notation  P ( X  =  A ) denotes the probability that a random variable  X takes the value  A. We introduce here an operator which enables to write this in Metamath as  ( P `  ( XRV/𝑐  _I  A ) ), and keep a similar notation. Because with this notation  ( XRV/𝑐  _I  A ) is a set, we can also apply it to conditional probabilities, like in  ( P `  ( XRV/𝑐  _I  A )  |  ( YRV/𝑐  _I  B ) ) ).

The oRVC operator transforms a relation  R into an operation taking a random variable  X and a constant  C, and returning the preimage through  X of the equivalence class of  C.

The most commonly used relations are: - equality:  { X  =  A } as  ( XRV/𝑐  _I  A ) cf. ideq 5144- elementhood:  { X  e.  A } as  ( XRV/𝑐  _E  A ) cf. epel 4783- less-than:  { X  <_  A } as  ( XRV/𝑐  <_  A )

Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g. for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.)

Assertion
Ref Expression
df-orvc  |-RV/𝑐 R  =  ( x  e.  { x  |  Fun  x } , 
a  e.  _V  |->  ( `' x " { y  |  y R a } ) )
Distinct variable group:    x, a, y, R

Detailed syntax breakdown of Definition df-orvc
StepHypRef Expression
1 cR . . 3  class  R
21corvc 28658 . 2  classRV/𝑐 R
3 vx . . 3  setvar  x
4 va . . 3  setvar  a
53cv 1397 . . . . 5  class  x
65wfun 5564 . . . 4  wff  Fun  x
76, 3cab 2439 . . 3  class  { x  |  Fun  x }
8 cvv 3106 . . 3  class  _V
95ccnv 4987 . . . 4  class  `' x
10 vy . . . . . . 7  setvar  y
1110cv 1397 . . . . . 6  class  y
124cv 1397 . . . . . 6  class  a
1311, 12, 1wbr 4439 . . . . 5  wff  y R a
1413, 10cab 2439 . . . 4  class  { y  |  y R a }
159, 14cima 4991 . . 3  class  ( `' x " { y  |  y R a } )
163, 4, 7, 8, 15cmpt2 6272 . 2  class  ( x  e.  { x  |  Fun  x } , 
a  e.  _V  |->  ( `' x " { y  |  y R a } ) )
172, 16wceq 1398 1  wffRV/𝑐 R  =  ( x  e.  { x  |  Fun  x } , 
a  e.  _V  |->  ( `' x " { y  |  y R a } ) )
Colors of variables: wff setvar class
This definition is referenced by:  orvcval  28660
  Copyright terms: Public domain W3C validator