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/𝑐 , and
keep a similar notation. Because with this notation ∘RV/𝑐
is a set, we can also apply it to conditional probabilities, like in
∘RV/𝑐 ∘RV/𝑐 .
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/𝑐 cf. ideq 5274-
elementhood: as
∘RV/𝑐 cf. epel 5032-
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.) |