---

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
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:ℕ. (((λp.if (A p =z 1) then 1 else B p fi ) <n, s>) = 1 ∈ ℤ)
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))

2
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:ℕ. ((A <n, s>) = 1 ∈ ℤ)
⊢ ∃n:ℕ. (if (A <n, s> =z 1) then 1 else B <n, s> fi  = 1 ∈ ℤ)

3
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:ℕ. ((B <n, s>) = 1 ∈ ℤ)
⊢ ∃n:ℕ. (if (A <n, s> =z 1) then 1 else B <n, s> fi  = 1 ∈ ℤ)

---

Latex:

---

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

---

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

---

Home Index