| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-orvc | Structured version Visualization version GIF version | ||
| 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 5863- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5587- 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.) |
| Ref | Expression |
|---|---|
| df-orvc | ⊢ ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cR | . . 3 class 𝑅 | |
| 2 | 1 | corvc 34458 | . 2 class ∘RV/𝑐𝑅 |
| 3 | vx | . . 3 setvar 𝑥 | |
| 4 | va | . . 3 setvar 𝑎 | |
| 5 | 3 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5 | wfun 6555 | . . . 4 wff Fun 𝑥 |
| 7 | 6, 3 | cab 2714 | . . 3 class {𝑥 ∣ Fun 𝑥} |
| 8 | cvv 3480 | . . 3 class V | |
| 9 | 5 | ccnv 5684 | . . . 4 class ◡𝑥 |
| 10 | vy | . . . . . . 7 setvar 𝑦 | |
| 11 | 10 | cv 1539 | . . . . . 6 class 𝑦 |
| 12 | 4 | cv 1539 | . . . . . 6 class 𝑎 |
| 13 | 11, 12, 1 | wbr 5143 | . . . . 5 wff 𝑦𝑅𝑎 |
| 14 | 13, 10 | cab 2714 | . . . 4 class {𝑦 ∣ 𝑦𝑅𝑎} |
| 15 | 9, 14 | cima 5688 | . . 3 class (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎}) |
| 16 | 3, 4, 7, 8, 15 | cmpo 7433 | . 2 class (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})) |
| 17 | 2, 16 | wceq 1540 | 1 wff ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})) |
| Colors of variables: wff setvar class |
| This definition is referenced by: orvcval 34460 |
| Copyright terms: Public domain | W3C validator |