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