{ 
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
Definitions :
all: x:A. B[x],
normal-type: Normal(T),
member: t 
T,
p-outcome: Outcome,
and: P 
Q,
length: ||as||,
int_seg: {i..j
},
ycomb: Y,
lelt: i 
j < k,
le: A B,
not: 
A,
implies: P 
Q,
false: False,
top: Top,
subtype: S 
T,
iff: P 
Q,
so_lambda: 
x.t[x],
rev_implies: P Q,
finite-prob-space: FinProbSpace,
prop: 
,
so_apply: x[s]
Lemmas :
finite-prob-space_wf,
le_wf,
length_wf1,
rationals_wf,
non_neg_length,
length_wf_nat,
top_wf,
int_seg_wf,
sum_unroll_base_q,
int-eq-in-rationals
\mforall{}p:FinProbSpace. Normal(Outcome)
Date html generated:
2010_08_27-AM-12_03_59
Last ObjectModification:
2009_03_20-AM-01_38_18
Home
Index