---

Step * of Lemma not-nullset

∀[p:FinProbSpace]. ¬nullset(p;λs.True) supposing ¬¬Konig(||p||)
BY
{ (Auto
   THEN (SupposeMore (-1) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Assert ∃C:p-open(p). ((∀s:ℕ ⟶ Outcome. s ∈ C) ∧ measure(C) ≤ (1/2)) BY
               (Unfold `nullset` -1
                THEN ((InstHyp [⌜(1/2)⌝] (-1))⋅ THENA Auto)
                THEN (Reduce (-1))
                THEN RepeatFor 3 (ParallelLast)
                THEN Auto))
   THEN ExRepD) }

1
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)
⊢ False

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mneg{}nullset(p;\mlambda{}s.True)  supposing  \mneg{}\mneg{}Konig(||p||)


By

---

Latex:
(Auto
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mexists{}C:p-open(p).  ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C)  \mwedge{}  measure(C)  \mleq{}  (1/2))  BY
                          (Unfold  `nullset`  -1
                            THEN  ((InstHyp  [\mkleeneopen{}(1/2)\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
                            THEN  (Reduce  (-1))
                            THEN  RepeatFor  3  (ParallelLast)
                            THEN  Auto))
  THEN  ExRepD)

---

Home Index