---

Step * of Lemma uniform-fps_wf

∀[n:ℕ+]. (uniform-fps(n) ∈ FinProbSpace)
BY
{ ((ProveWfLemma THEN Unfold `finite-prob-space` 0) THEN MemTypeCD THEN Auto) }

1
1. n : ℕ+
⊢ Σ0 ≤ i < n. map(λx.(1/n);upto(n))[i] = 1 ∈ ℚ

2
1. n : ℕ+
2. Σ0 ≤ i < ||map(λx.(1/n);upto(n))||. map(λx.(1/n);upto(n))[i] = 1 ∈ ℚ
⊢ (∀q∈map(λx.(1/n);upto(n)).0 ≤ q)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (uniform-fps(n)  \mmember{}  FinProbSpace)


By

---

Latex:
((ProveWfLemma  THEN  Unfold  `finite-prob-space`  0)  THEN  MemTypeCD  THEN  Auto)

---

Home Index