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