Nuprl Lemma : uniform-fps_wf
∀[n:ℕ+]. (uniform-fps(n) ∈ FinProbSpace)
Proof
Definitions occuring in Statement :
uniform-fps: uniform-fps(n),
finite-prob-space: FinProbSpace,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
rationals_wf,
Error :qsum-const,
nat_plus_subtype_nat,
qdiv_wf,
int-subtype-rationals,
subtype_rel_set,
less_than_wf,
Error :int_nzero-rational,
subtype_rel_sets,
nequal_wf,
less_than_transitivity1,
le_weakening,
less_than_irreflexivity,
equal_wf,
equal-wf-base,
int_subtype_base,
iff_weakening_equal,
Error :qmul-qdiv-cancel,
squash_wf,
true_wf,
Error :qsum_wf,
int_seg_wf,
select-map,
upto_wf,
subtype_rel_list,
top_wf,
length_upto,
lelt_wf,
length_wf,
map_wf,
non_neg_length,
length_wf_nat,
map_length,
Error :qinv-nonneg,
Error :qless-int
\mforall{}[n:\mBbbN{}\msupplus{}]. (uniform-fps(n) \mmember{} FinProbSpace)
Date html generated:
2015_07_17-AM-07_58_05
Last ObjectModification:
2015_02_03-PM-09_44_30
Home
Index