---

Step * 1 1 1 1 1 of Lemma expectation-imax-list


1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
5. s : ℕn ─→ Outcome@i
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
⊢ (∀b∈map(λi.(X i s);upto(k)).b ≤ Σ0 ≤ i < k. X i s)
BY
{ ((BLemma `l_all_iff` THENA Auto)
   THEN (RWO "member_map" 0 THENA (Auto THEN Reduce 0 THEN Auto))
   THEN Reduce 0
   THEN Auto
   THEN ExRepD) }

1
1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
5. s : ℕn ─→ Outcome@i
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
8. b : ℕ@i
9. y : ℕk@i
10. (y ∈ upto(k))@i
11. b = (X y s) ∈ ℕ@i
⊢ b ≤ Σ0 ≤ i < k. X i s

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbN{}
3.  k  :  \mBbbN{}\msupplus{}
4.  X  :  \mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbN{}
5.  s  :  \mBbbN{}n  {}\mrightarrow{}  Outcome@i
6.  0  <  ||map(\mlambda{}i.(X  i  s);upto(k))||
7.  \mSigma{}0  \mleq{}  i  <  k.  X  i  s  \mmember{}  \mBbbZ{}
\mvdash{}  (\mforall{}b\mmember{}map(\mlambda{}i.(X  i  s);upto(k)).b  \mleq{}  \mSigma{}0  \mleq{}  i  <  k.  X  i  s)


By

((BLemma  `l\_all\_iff`  THENA  Auto)
  THEN  (RWO  "member\_map"  0  THENA  (Auto  THEN  Reduce  0  THEN  Auto))
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index