---

Step * of Lemma member-countable-p-union

∀p:FinProbSpace. ∀A:ℕ ─→ p-open(p). ∀s:ℕ ─→ Outcome.  ((∃i:ℕ. s ∈ A[i]) ⇒ s ∈ countable-p-union(i.A[i]))
BY
{ (Auto THEN ((Unfold `p-open-member` (-1) THEN ExRepD) THEN Unfold `p-open-member` 0)⋅) }

1
1. p : FinProbSpace@i
2. A : ℕ ─→ p-open(p)@i
3. s : ℕ ─→ Outcome@i
4. i : ℕ@i
5. n : ℕ@i
6. (A[i] <n, s>) = 1 ∈ ℤ@i
⊢ ∃n:ℕ. ((countable-p-union(i.A[i]) <n, s>) = 1 ∈ ℤ)

---

Latex:


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


By

(Auto  THEN  ((Unfold  `p-open-member`  (-1)  THEN  ExRepD)  THEN  Unfold  `p-open-member`  0)\mcdot{})

---

Home Index