Nuprl Lemma : normal-p-outcome
∀p:FinProbSpace. Normal(Outcome)
Proof
Definitions occuring in Statement :
normal-type: Normal(T),
all: ∀x:A. B[x],
p-outcome: Outcome,
finite-prob-space: FinProbSpace
Lemmas :
false_wf,
lelt_wf,
length_wf,
rationals_wf,
finite-prob-space_wf,
list-cases,
length_of_nil_lemma,
stuck-spread,
base_wf,
product_subtype_list,
length_of_cons_lemma,
non_neg_length,
length_wf_nat,
less_than_transitivity1,
less_than_irreflexivity,
int_seg_wf,
int-eq-in-rationals,
not_wf,
less_than_wf,
Error :sum_unroll_base_q,
iff_weakening_equal
\mforall{}p:FinProbSpace. Normal(Outcome)
Date html generated:
2015_07_17-AM-11_18_51
Last ObjectModification:
2015_02_04-PM-05_05_55
Home
Index