---

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
2. A : ℕ ⟶ p-open(p)
3. s : ℕ ⟶ Outcome
4. i : ℕ
5. n : ℕ
6. (A[i] <n, s>) = 1 ∈ ℤ
⊢ ∃n:ℕ. ((countable-p-union(i.A[i]) <n, s>) = 1 ∈ ℤ)

---

Latex:

---

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

---

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

---

Home Index