---

Step * of Lemma countable-p-union_wf

∀[p:FinProbSpace]. ∀[A:ℕ ─→ p-open(p)].  (countable-p-union(i.A[i]) ∈ p-open(p))
BY
{ (Unfolds ``p-open countable-p-union`` 0⋅ THEN (Auto THEN MemTypeCD) THEN skip{(MemTypeCD THEN Auto THEN Reduce 0)})⋅ }

1
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
⊢ λp.if (fst(p) =z 0) then 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi  ∈ (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2

2
.....set predicate..... 
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
⊢ ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.
    (((λp.if (fst(p) =z 0) then 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi ) <i, s>) ≤ ((λp.if (fst(p) =z 0) the\000Cn 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi ) <j, s>))

3
.....wf..... 
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. C : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2
⊢ ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>)) ∈ Type

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[A:\mBbbN{}  {}\mrightarrow{}  p-open(p)].    (countable-p-union(i.A[i])  \mmember{}  p-open(p))


By

(Unfolds  ``p-open  countable-p-union``  0\mcdot{}
  THEN  (Auto  THEN  MemTypeCD)
  THEN  skip\{(MemTypeCD  THEN  Auto  THEN  Reduce  0)\})\mcdot{}

---

Home Index