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)


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: supposing a uall: [x:A]. B[x] or: P ∨ Q member: t ∈ T set: {x:A| B[x]}  apply: a pair: <a, b> natural_number: $n int: equal: 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