Nuprl Lemma : rv-disjoint-rv-mul

p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;Z)  rv-disjoint(p;n;X;Y Z))


Proof




Definitions occuring in Statement :  rv-disjoint: rv-disjoint(p;n;X;Y) rv-mul: Y random-variable: RandomVariable(p;n) finite-prob-space: FinProbSpace nat: all: x:A. B[x] implies:  Q
Lemmas :  all_wf p-outcome_wf not_wf equal_wf rationals_wf rv-mul_wf qmul_wf int_seg_wf rv-disjoint_wf random-variable_wf nat_wf finite-prob-space_wf
\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y,Z:RandomVariable(p;n).
    (rv-disjoint(p;n;X;Y)  {}\mRightarrow{}  rv-disjoint(p;n;X;Z)  {}\mRightarrow{}  rv-disjoint(p;n;X;Y  *  Z))



Date html generated: 2015_07_17-AM-07_59_10
Last ObjectModification: 2015_01_27-AM-11_22_57

Home Index