---

Step * 1 of Lemma member-countable-p-union


1. p : FinProbSpace@i
2. A : ℕ ─→ p-open(p)@i
3. s : ℕ ─→ Outcome@i
4. i : ℕ@i
5. n : ℕ@i
6. (A[i] <n, s>) = 1 ∈ ℤ@i
⊢ ∃n:ℕ. ((countable-p-union(i.A[i]) <n, s>) = 1 ∈ ℤ)
BY
{ (Assert ∃m:ℕ. (i < m ∧ n < m) BY
         (InstConcl [⌈if i <z n then n + 1 else i + 1 fi ⌉]⋅ THEN Auto THEN SplitOnConclITE THEN Auto')) }

1
1. p : FinProbSpace@i
2. A : ℕ ─→ p-open(p)@i
3. s : ℕ ─→ Outcome@i
4. i : ℕ@i
5. n : ℕ@i
6. (A[i] <n, s>) = 1 ∈ ℤ@i
7. ∃m:ℕ. (i < m ∧ n < m)
⊢ ∃n:ℕ. ((countable-p-union(i.A[i]) <n, s>) = 1 ∈ ℤ)

---

Latex:



1.  p  :  FinProbSpace@i
2.  A  :  \mBbbN{}  {}\mrightarrow{}  p-open(p)@i
3.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome@i
4.  i  :  \mBbbN{}@i
5.  n  :  \mBbbN{}@i
6.  (A[i]  <n,  s>)  =  1@i
\mvdash{}  \mexists{}n:\mBbbN{}.  ((countable-p-union(i.A[i])  <n,  s>)  =  1)


By

(Assert  \mexists{}m:\mBbbN{}.  (i  <  m  \mwedge{}  n  <  m)  BY
              (InstConcl  [\mkleeneopen{}if  i  <z  n  then  n  +  1  else  i  +  1  fi  \mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  SplitOnConclITE
                THEN  Auto'))

---

Home Index