Nuprl Lemma : fps-not-null
∀[p:FinProbSpace]. (null(p) ~ ff)
Proof
Definitions occuring in Statement :
finite-prob-space: FinProbSpace,
null: null(as),
bfalse: ff,
uall: ∀[x:A]. B[x],
sqequal: s ~ t
Lemmas :
rationals_wf,
list-cases,
null_nil_lemma,
subtype_base_sq,
bool_wf,
bool_subtype_base,
btrue_wf,
ppcc-problem,
unit_wf2,
iff_imp_equal_bool,
bfalse_wf,
assert-qeq,
true_wf,
false_wf,
iff_weakening_equal,
product_subtype_list,
null_cons_lemma,
finite-prob-space_wf
\mforall{}[p:FinProbSpace]. (null(p) \msim{} ff)
Date html generated:
2015_07_17-AM-07_57_55
Last ObjectModification:
2015_02_03-PM-09_44_10
Home
Index