---

Step * 1 2 2 1 of Lemma countable-p-union_wf


1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. n : ℕ@i
4. p2 : ℕn ─→ Outcome@i
5. ¬(n = 0 ∈ ℤ)
⊢ (∀b∈map(λi.(A[i] <n, p2>);upto(n)).b ≤ 1)
BY
{ (BLemma `l_all_iff` THEN Auto THEN RWO "member_map" (-1)⋅ THEN Auto THEN Reduce (-1) THEN ExRepD THEN Auto') }

---

Latex:



1.  p  :  FinProbSpace
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \{C:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2|  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>\000C))\} 
3.  n  :  \mBbbN{}@i
4.  p2  :  \mBbbN{}n  {}\mrightarrow{}  Outcome@i
5.  \mneg{}(n  =  0)
\mvdash{}  (\mforall{}b\mmember{}map(\mlambda{}i.(A[i]  <n,  p2>);upto(n)).b  \mleq{}  1)


By

(BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  RWO  "member\_map"  (-1)\mcdot{}
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  ExRepD
  THEN  Auto')

---

Home Index