Nuprl Lemma : rv-mul_wf

[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X Y ∈ RandomVariable(k;n))


Proof




Definitions occuring in Statement :  rv-mul: Y random-variable: RandomVariable(p;n) finite-prob-space: FinProbSpace nat: uall: [x:A]. B[x] member: t ∈ T
Lemmas :  qmul_wf int_seg_wf length_wf rationals_wf nat_wf set_wf list_wf equal-wf-T-base Error :qsum_wf,  select_wf sq_stable__le l_all_wf2 l_member_wf Error :qle_wf,  int-subtype-rationals
\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(k;n)].    (X  *  Y  \mmember{}  RandomVariable(k;n))



Date html generated: 2015_07_17-AM-07_58_42
Last ObjectModification: 2015_01_27-AM-11_23_52

Home Index