---

Step * 1 1 1 1 1 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
7. m : ℕ
8. i < m
9. n < m
10. ¬(m = 0 ∈ ℤ)
⊢ (∃b∈map(λi.(A[i] <m, s>);upto(m)). 1 ≤ b)
BY
{ ((BLemma `l_exists_iff` THEN Auto)
   THEN InstConcl[⌈1⌉]⋅
   THEN Auto
   THEN RWO "member_map" 0
   THEN Auto
   THEN Reduce 0
   THEN InstConcl [⌈i⌉]⋅
   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 : ℕ
8. i < m
9. n < m
10. ¬(m = 0 ∈ ℤ)
⊢ (i ∈ upto(m))

2
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 : ℕ
8. i < m
9. n < m
10. ¬(m = 0 ∈ ℤ)
11. (i ∈ upto(m))
⊢ 1 = (A[i] <m, s>) ∈ ℕ2

---

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
7.  m  :  \mBbbN{}
8.  i  <  m
9.  n  <  m
10.  \mneg{}(m  =  0)
\mvdash{}  (\mexists{}b\mmember{}map(\mlambda{}i.(A[i]  <m,  s>);upto(m)).  1  \mleq{}  b)


By

((BLemma  `l\_exists\_iff`  THEN  Auto)
  THEN  InstConcl[\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWO  "member\_map"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index