---

Step * of 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 ∈ ℤ)))
BY
{ (At ⌈Type⌉ Auto⋅ THEN (InstConcl [⌈find-random{2}(C;p;a;b)⌉]⋅ THENA Auto)) }

1
.....set predicate..... 
1. p : FinProbSpace@i
2. a : Atom2@i
3. b : Atom2@i
4. C : p-open(p)@i
5. measure(C) = 1@i
6. a#C:p-open(p) ∨ b#C:p-open(p)@i
⊢ 0 ≤ find-random{2}(C;p;a;b)

2
1. p : FinProbSpace@i
2. a : Atom2@i
3. b : Atom2@i
4. C : p-open(p)@i
5. measure(C) = 1@i
6. a#C:p-open(p) ∨ b#C:p-open(p)@i
⊢ (C <find-random{2}(C;p;a;b), random(p;a;b)>) = 1 ∈ ℤ

---

Latex:


\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)))


By

(At  \mkleeneopen{}Type\mkleeneclose{}  Auto\mcdot{}  THEN  (InstConcl  [\mkleeneopen{}find-random\{2\}(C;p;a;b)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index