---

Step * 1 2 1 2 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 : ℕ
4. p2 : ℕn ⟶ Outcome
5. ¬(n = 0 ∈ ℤ)
⊢ imax-list(map(λi.(A[i] <n, p2>);upto(n))) < 2
BY
{ xxx((Assert imax-list(map(λi.(A[i] <n, p2>);upto(n))) ≤ 1 BY
             (BLemma `imax-list-lb` THEN Auto))
      THEN Auto
      THEN Try (((RWO "length-map" 0 THENA Auto) THEN RWO "length_upto" 0 THEN Auto)))xxx }

1
1. p : FinProbSpace
2. A : ℕ ⟶ {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. n : ℕ
4. p2 : ℕn ⟶ Outcome
5. ¬(n = 0 ∈ ℤ)
⊢ (∀b∈map(λi.(A[i] <n, p2>);upto(n)).b ≤ 1)

---

Latex:

---

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{}
4.  p2  :  \mBbbN{}n  {}\mrightarrow{}  Outcome
5.  \mneg{}(n  =  0)
\mvdash{}  imax-list(map(\mlambda{}i.(A[i]  <n,  p2>);upto(n)))  <  2


By

---

Latex:
xxx((Assert  imax-list(map(\mlambda{}i.(A[i]  <n,  p2>);upto(n)))  \mleq{}  1  BY
                      (BLemma  `imax-list-lb`  THEN  Auto))
        THEN  Auto
        THEN  Try  (((RWO  "length-map"  0  THENA  Auto)  THEN  RWO  "length\_upto"  0  THEN  Auto)))xxx

---

Home Index