Metamath Proof Explorer

Definition df-orvc

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( X oRVCI A ) ) , and keep a similar notation. Because with this notation ( X oRVC I A ) is a set, we can also apply it to conditional probabilities, like in ( P( X oRVCI A ) | ( Y oRVC 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 ( X oRVCI A ) cf. ideq - elementhood: { X e. A } as ( X oRVC E A ) cf. epel - less-than: { X <_ A } as ( X oRVC <_ 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)

Ref Expression
Assertion df-orvc ⊢ ∘ RV/c ⁡ R = x ∈ x | Fun ⁡ x , a ∈ V ⟼ x -1 y | y R a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 0 corvc class ∘ RV/c ⁡ R
2 vx setvar x
3 2 cv setvar x
4 3 wfun wff Fun ⁡ x
5 4 2 cab class x | Fun ⁡ x
6 va setvar a
7 cvv class V
8 3 ccnv class x -1
9 vy setvar y
10 9 cv setvar y
11 6 cv setvar a
12 10 11 0 wbr wff y R a
13 12 9 cab class y | y R a
14 8 13 cima class x -1 y | y R a
15 2 6 5 7 14 cmpo class x ∈ x | Fun ⁡ x , a ∈ V ⟼ x -1 y | y R a
16 1 15 wceq wff ∘ RV/c ⁡ R = x ∈ x | Fun ⁡ x , a ∈ V ⟼ x -1 y | y R a