---

Step * of Lemma p-union_wf

∀[p:FinProbSpace]. ∀[A,B:p-open(p)].  (p-union(A;B) ∈ p-open(p))
BY
{ (Unfolds ``p-open p-union`` 0⋅ THEN Auto) }

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>))} 
⊢ λp.if (A p =z 1) then 1 else B p fi  ∈ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| 
                                          ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[A,B:p-open(p)].    (p-union(A;B)  \mmember{}  p-open(p))


By

(Unfolds  ``p-open  p-union``  0\mcdot{}  THEN  Auto)

---

Home Index