---

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


1. p : FinProbSpace
2. A : ℕ ⟶ p-open(p)
3. s : ℕ ⟶ Outcome
4. i : ℕ
5. n : ℕ
6. (A[i] <n, s>) = 1 ∈ ℤ
7. ∃m:ℕ. (i < m ∧ n < m)
⊢ ∃n:ℕ. ((countable-p-union(i.A[i]) <n, s>) = 1 ∈ ℤ)
BY
{ xxx(ParallelLast THEN Auto THEN Try ((DoSubsume THEN Auto)))xxx }

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(ParallelLast  THEN  Auto  THEN  Try  ((DoSubsume  THEN  Auto)))xxx

---

Home Index