---

Step * 1 1 of Lemma member-p-union

.....truecase..... 
1. p : FinProbSpace
2. A : {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. B : {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
4. s : ℕ ⟶ Outcome
5. n : ℕ
6. 1 = 1 ∈ ℤ
7. (A <n, s>) = 1 ∈ ℤ
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))
BY
{ ((OrLeft THEN Auto) THEN InstConcl [⌜n⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  p  :  FinProbSpace
2.  A  :  \{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>))\} 
3.  B  :  \{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>))\} 
4.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome
5.  n  :  \mBbbN{}
6.  1  =  1
7.  (A  <n,  s>)  =  1
\mvdash{}  (\mexists{}n:\mBbbN{}.  ((A  <n,  s>)  =  1))  \mvee{}  (\mexists{}n:\mBbbN{}.  ((B  <n,  s>)  =  1))


By

---

Latex:
((OrLeft  THEN  Auto)  THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index