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

Definition df-orvc 31063
 Description: Define the preimage set mapping operator. In probability theory, the notation 𝑃(𝑋 = 𝐴) denotes the probability that a random variable 𝑋 takes the value 𝐴. We introduce here an operator which enables to write this in Metamath as (𝑃‘(𝑋∘RV/𝑐 I 𝐴)), and keep a similar notation. Because with this notation (𝑋∘RV/𝑐 I 𝐴) is a set, we can also apply it to conditional probabilities, like in (𝑃‘(𝑋∘RV/𝑐 I 𝐴) ∣ (𝑌∘RV/𝑐 I 𝐵))). The oRVC operator transforms a relation 𝑅 into an operation taking a random variable 𝑋 and a constant 𝐶, and returning the preimage through 𝑋 of the equivalence class of 𝐶. The most commonly used relations are: - equality: {𝑋 = 𝐴} as (𝑋∘RV/𝑐 I 𝐴) cf. ideq 5506- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5257- less-than: {𝑋 ≤ 𝐴} as (𝑋∘RV/𝑐 ≤ 𝐴) 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/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (𝑥 “ {𝑦𝑦𝑅𝑎}))
Distinct variable group:   𝑥,𝑎,𝑦,𝑅

Detailed syntax breakdown of Definition df-orvc
StepHypRef Expression
1 cR . . 3 class 𝑅
21corvc 31062 . 2 class RV/𝑐𝑅
3 vx . . 3 setvar 𝑥
4 va . . 3 setvar 𝑎
53cv 1657 . . . . 5 class 𝑥
65wfun 6116 . . . 4 wff Fun 𝑥
76, 3cab 2810 . . 3 class {𝑥 ∣ Fun 𝑥}
8 cvv 3413 . . 3 class V
95ccnv 5340 . . . 4 class 𝑥
10 vy . . . . . . 7 setvar 𝑦
1110cv 1657 . . . . . 6 class 𝑦
124cv 1657 . . . . . 6 class 𝑎
1311, 12, 1wbr 4872 . . . . 5 wff 𝑦𝑅𝑎
1413, 10cab 2810 . . . 4 class {𝑦𝑦𝑅𝑎}
159, 14cima 5344 . . 3 class (𝑥 “ {𝑦𝑦𝑅𝑎})
163, 4, 7, 8, 15cmpt2 6906 . 2 class (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (𝑥 “ {𝑦𝑦𝑅𝑎}))
172, 16wceq 1658 1 wff RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (𝑥 “ {𝑦𝑦𝑅𝑎}))
 Colors of variables: wff setvar class This definition is referenced by:  orvcval  31064
 Copyright terms: Public domain W3C validator