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