---

Step * 1 1 1 1 1 2 of Lemma not-nullset


1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2
4. ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))
5. ∀s:ℕ ─→ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
7. ∀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>))))@i
8. i : ℕ@i
9. j : ℕ@i
10. i ≤ j@i
11. x : ℕj ─→ Outcome@i
12. (C <j, x>) = 0 ∈ ℤ
13. ¬(i = j ∈ ℤ)
⊢ (C <i, λn.if n <z j then x n else 0 fi >) ≤ (C <j, λn.if n <z j then x n else 0 fi >)
BY
{ Auto' }

---

Latex:



1.  p  :  FinProbSpace
2.  nullset(p;\mlambda{}s.True)@i
3.  C  :  (n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2
4.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>))
5.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C
6.  measure(C)  \mleq{}  (1/2)
7.  \mforall{}tree:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbB{}
          ((\mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}j  {}\mrightarrow{}  Outcome.  ((\muparrow{}(tree  <j,  x>))  {}\mRightarrow{}  (\muparrow{}(tree  <i,  x>))))))
          {}\mRightarrow{}  (\mneg{}(\mexists{}b:\mBbbN{}.  \mforall{}x:\mBbbN{}b  {}\mrightarrow{}  Outcome.  (\mneg{}\muparrow{}(tree  <b,  x>))))
          {}\mRightarrow{}  (\mexists{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}.  (\muparrow{}(tree  <n,  s>))))@i
8.  i  :  \mBbbN{}@i
9.  j  :  \mBbbN{}@i
10.  i  \mleq{}  j@i
11.  x  :  \mBbbN{}j  {}\mrightarrow{}  Outcome@i
12.  (C  <j,  x>)  =  0
13.  \mneg{}(i  =  j)
\mvdash{}  (C  <i,  \mlambda{}n.if  n  <z  j  then  x  n  else  0  fi  >)  \mleq{}  (C  <j,  \mlambda{}n.if  n  <z  j  then  x  n  else  0  fi  >)


By

Auto'

---

Home Index