---

Step * 1 1 of Lemma not-nullset

.....assertion..... 
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)
⊢ ∃s:ℕ ⟶ Outcome. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)
BY
{ (Unfold `Konig` 2 THEN Fold `p-outcome` 2 THEN InstHyp [⌜λp.(C p =z 0)⌝] 2⋅ THEN All Reduce THEN Auto) }

1
1. p : FinProbSpace
2. ∀tree:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ⟶ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(tree <n, s>))))
3. nullset(p;λs.True)
4. C : p-open(p)
5. ∀s:ℕ ⟶ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
7. i : ℕ
8. j : ℕ
9. i ≤ j
10. x : ℕj ⟶ Outcome
11. ↑(C <j, x> =z 0)
⊢ (C <i, x>) = 0 ∈ ℤ

2
1. p : FinProbSpace
2. ∀tree:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ⟶ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(tree <n, s>))))
3. nullset(p;λs.True)
4. C : p-open(p)
5. ∀s:ℕ ⟶ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
⊢ ¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(C <b, x> =z 0)))

3
1. p : FinProbSpace
2. ∀tree:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ⟶ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(tree <n, s>))))
3. nullset(p;λs.True)
4. C : p-open(p)
5. ∀s:ℕ ⟶ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
7. ∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(C <n, s> =z 0))
⊢ ∃s:ℕ ⟶ Outcome. ∀n:ℕ. ((C <n, s>) = 0 ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  \mexists{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}.  ((C  <n,  s>)  =  0)


By

---

Latex:
(Unfold  `Konig`  2
  THEN  Fold  `p-outcome`  2
  THEN  InstHyp  [\mkleeneopen{}\mlambda{}p.(C  p  =\msubz{}  0)\mkleeneclose{}]  2\mcdot{}
  THEN  All  Reduce
  THEN  Auto)

---

Home Index