---

Step * 1 1 1 1 2 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 : ℕ
8. i < m
9. n < m
10. ¬(m = 0 ∈ ℤ)
11. 1 ≤ imax-list(map(λi.(A[i] <m, s>);upto(m)))
⊢ imax-list(map(λi.(A[i] <m, s>);upto(m))) = 1 ∈ ℤ
BY
{ Assert ⌜imax-list(map(λi.(A[i] <m, s>);upto(m))) ≤ 1⌝⋅ }

1
.....assertion..... 
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
10. ¬(m = 0 ∈ ℤ)
11. 1 ≤ imax-list(map(λi.(A[i] <m, s>);upto(m)))
⊢ imax-list(map(λi.(A[i] <m, s>);upto(m))) ≤ 1

2
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
10. ¬(m = 0 ∈ ℤ)
11. 1 ≤ imax-list(map(λi.(A[i] <m, s>);upto(m)))
12. imax-list(map(λi.(A[i] <m, s>);upto(m))) ≤ 1
⊢ imax-list(map(λi.(A[i] <m, s>);upto(m))) = 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.  m  :  \mBbbN{}
8.  i  <  m
9.  n  <  m
10.  \mneg{}(m  =  0)
11.  1  \mleq{}  imax-list(map(\mlambda{}i.(A[i]  <m,  s>);upto(m)))
\mvdash{}  imax-list(map(\mlambda{}i.(A[i]  <m,  s>);upto(m)))  =  1


By

---

Latex:
Assert  \mkleeneopen{}imax-list(map(\mlambda{}i.(A[i]  <m,  s>);upto(m)))  \mleq{}  1\mkleeneclose{}\mcdot{}

---

Home Index