---

Step * of Lemma member-p-union

∀p:FinProbSpace. ∀A,B:p-open(p). ∀s:ℕ ─→ Outcome.  (s ∈ p-union(A;B) ⇐⇒ s ∈ A ∨ s ∈ B)
BY
{ (Unfolds ``p-open-member p-open p-union`` 0 THEN Auto THEN Reduce 0 THEN Auto' THEN SplitOrHyps)⋅ }

1
1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. ∃n:ℕ. (((λp.if (A p =z 1) then 1 else B p fi ) <n, s>) = 1 ∈ ℤ)@i
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))

2
1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. ∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)@i
⊢ ∃n:ℕ. (if (A <n, s> =z 1) then 1 else B <n, s> fi  = 1 ∈ ℤ)

3
1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. ∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ)@i
⊢ ∃n:ℕ. (if (A <n, s> =z 1) then 1 else B <n, s> fi  = 1 ∈ ℤ)

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}A,B:p-open(p).  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.    (s  \mmember{}  p-union(A;B)  \mLeftarrow{}{}\mRightarrow{}  s  \mmember{}  A  \mvee{}  s  \mmember{}  B)


By

(Unfolds  ``p-open-member  p-open  p-union``  0  THEN  Auto  THEN  Reduce  0  THEN  Auto'  THEN  SplitOrHyps)\mcdot{}

---

Home Index