### Nuprl Lemma : randomness

`∀p:FinProbSpace. ∀a,b:Atom2. ∀C:p-open(p).`
`  (measure(C) = 1 `` (a#C:p-open(p) ∨ b#C:p-open(p)) `` (∃n:ℕ. ((C <n, random(p;a;b)>) = 1 ∈ ℤ)))`

Proof

Definitions occuring in Statement :  random: `random(p;a;b)` p-open-measure-one: `measure(C) = 1` p-open: `p-open(p)` finite-prob-space: `FinProbSpace` nat: `ℕ` free-from-atom: `a#x:T` atom: `Atom\$n` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` apply: `f a` pair: `<a, b>` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Lemmas :  find-random_wf nat_wf subtype_rel_dep_function p-outcome_wf int_seg_wf int_seg_subtype-nat false_wf subtype_rel_self le_wf equal-wf-T-base random_wf or_wf free-from-atom_wf2 p-open_wf p-open-measure-one_wf finite-prob-space_wf set_wf sq_stable__le equal_wf
\mforall{}p:FinProbSpace.  \mforall{}a,b:Atom2.  \mforall{}C:p-open(p).
(measure(C)  =  1  {}\mRightarrow{}  (a\#C:p-open(p)  \mvee{}  b\#C:p-open(p))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  ((C  <n,  random(p;a;b)>)  =  1)))

Date html generated: 2015_07_17-AM-08_04_32
Last ObjectModification: 2015_01_27-AM-11_24_45

Home Index