Nuprl Lemma : rv-add_wf
∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)]. (X + Y ∈ RandomVariable(k;n))
Proof
Definitions occuring in Statement :
rv-add: X + Y,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
rv-add: X + Y,
nat: ℕ
Lemmas referenced :
qadd_wf,
int_seg_wf,
length_wf,
rationals_wf,
random-variable_wf,
istype-nat,
finite-prob-space_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalHypSubstitution,
lambdaEquality_alt,
introduction,
extract_by_obid,
isectElimination,
thin,
applyEquality,
hypothesisEquality,
hypothesis,
functionIsType,
universeIsType,
natural_numberEquality,
setElimination,
rename,
because_Cache
Latex:
\mforall{}[k:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X,Y:RandomVariable(k;n)]. (X + Y \mmember{} RandomVariable(k;n))
Date html generated:
2020_05_20-AM-09_31_21
Last ObjectModification:
2019_11_27-PM-05_07_57
Theory : randomness
Home
Index