### Nuprl Lemma : rv-unbounded_wf

`∀[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  ((X[n]─→∞ as n─→∞) ∈ (ℕ ─→ Outcome) ─→ ℙ)`

Proof

Definitions occuring in Statement :  rv-unbounded: `(X[n]─→∞ as n─→∞)` random-variable: `RandomVariable(p;n)` p-outcome: `Outcome` finite-prob-space: `FinProbSpace` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ─→ B[x]`
Lemmas :  all_wf rationals_wf exists_wf le_wf Error :qle_wf,  random-variable_wf subtype_rel_dep_function p-outcome_wf int_seg_wf nat_wf length_wf int_seg_subtype-nat false_wf finite-prob-space_wf
\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].
((X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{})  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{})

Date html generated: 2015_07_17-AM-08_01_25
Last ObjectModification: 2015_01_27-AM-11_21_55

Home Index