### Nuprl Lemma : find-random_wf

`∀[p:FinProbSpace]. ∀[a,b:Atom2]. ∀[C:p-open(p)].`
`  (find-random{2}(C;p;a;b) ∈ {n:ℕ| (C <n, random(p;a;b)>) = 1 ∈ ℤ} ) supposing ((a#C:p-open(p) ∨ b#C:p-open(p)) and meas\000Cure(C) = 1)`

Proof

Definitions occuring in Statement :  find-random: `find-random{\$k}(C;p;a;b)` 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` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` or: `P ∨ Q` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` pair: `<a, b>` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Lemmas :  or_wf free-from-atom_wf2 p-open-measure-one_wf p-open_wf finite-prob-space_wf
\mforall{}[p:FinProbSpace].  \mforall{}[a,b:Atom2].  \mforall{}[C:p-open(p)].
(find-random\{2\}(C;p;a;b)  \mmember{}  \{n:\mBbbN{}|  (C  <n,  random(p;a;b)>)  =  1\}  )  supposing  ((a\#C:p-open(p)  \mvee{}  b\#C:p-o\000Cpen(p))  and  measure(C)  =  1)

Date html generated: 2015_07_17-AM-08_04_30
Last ObjectModification: 2015_01_27-AM-11_22_08

Home Index