---

Step * 1 1 1 1 1 1 2 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. m : ℕ
7. i < m
8. n < m
9. ¬(m = 0 ∈ ℤ)
10. (i ∈ upto(m))
11. v : p-open(p)@i
12. A[i] = v ∈ p-open(p)@i
⊢ ((v <n, s>) = 1 ∈ ℤ) ⇒ (1 = (v <m, s>) ∈ ℕ2)
BY
{ (Auto THEN DVar `v' THEN Auto THEN InstHyp [⌈s⌉;⌈m⌉;⌈n⌉] (-3)⋅ THEN Auto') }

---

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.  m  :  \mBbbN{}
7.  i  <  m
8.  n  <  m
9.  \mneg{}(m  =  0)
10.  (i  \mmember{}  upto(m))
11.  v  :  p-open(p)@i
12.  A[i]  =  v@i
\mvdash{}  ((v  <n,  s>)  =  1)  {}\mRightarrow{}  (1  =  (v  <m,  s>))


By

(Auto  THEN  DVar  `v'  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto')

---

Home Index