---

Step * 1 of Lemma not-nullset


1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. measure(C) ≤ (1/2)
6. Konig(||p||)@i
⊢ False
BY
{ Assert ⌈∃s:ℕ ─→ Outcome. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)⌉⋅ }

1
.....assertion..... 
1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. measure(C) ≤ (1/2)
6. Konig(||p||)@i
⊢ ∃s:ℕ ─→ Outcome. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)

2
1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. measure(C) ≤ (1/2)
6. Konig(||p||)@i
7. ∃s:ℕ ─→ Outcome. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)
⊢ False

---

Latex:



1.  p  :  FinProbSpace
2.  nullset(p;\mlambda{}s.True)@i
3.  C  :  p-open(p)
4.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C
5.  measure(C)  \mleq{}  (1/2)
6.  Konig(||p||)@i
\mvdash{}  False


By

Assert  \mkleeneopen{}\mexists{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}.  ((C  <n,  s>)  =  0)\mkleeneclose{}\mcdot{}

---

Home Index