---

Step * 1 of Lemma random_wf


1. p : FinProbSpace
2. a : Atom2
3. b : Atom2
⊢ random(p;a;b) ∈ ℕ ─→ Outcome
BY
{ Unfold `member` 0 }

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

---

Latex:



1.  p  :  FinProbSpace
2.  a  :  Atom2
3.  b  :  Atom2
\mvdash{}  random(p;a;b)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  Outcome


By

Unfold  `member`  0

---

Home Index