---

Step * of Lemma random_wf

∀[p:FinProbSpace]. ∀[a,b:Atom2].  (random(p;a;b) ∈ ℕ ─→ Outcome)
BY
{ Auto }

1
1. p : FinProbSpace
2. a : Atom2
3. b : Atom2
⊢ random(p;a;b) ∈ ℕ ─→ Outcome

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[a,b:Atom2].    (random(p;a;b)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  Outcome)


By

Auto

---

Home Index