---

Step * 1 2 1 of Lemma not-nullset


1. p : FinProbSpace
2. Konig(||p||)
3. nullset(p;λs.True)
4. C : p-open(p)
5. ∀s:ℕ ⟶ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
7. s : ℕ ⟶ Outcome
8. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)
9. s ∈ C
⊢ False
BY
{ (D -1 THEN InstHyp [⌜n⌝] (-3)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  Konig(||p||)
3.  nullset(p;\mlambda{}s.True)
4.  C  :  p-open(p)
5.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C
6.  measure(C)  \mleq{}  (1/2)
7.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome
8.  \mforall{}n:\mBbbN{}.  ((C  <n,  s>)  =  0)
9.  s  \mmember{}  C
\mvdash{}  False


By

---

Latex:
(D  -1  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto')

---

Home Index