Nuprl Lemma : isempty_lemma
∀e,eo:Top. (e ∈b Empty ~ ff)
Proof
Definitions occuring in Statement :
es-empty-interface: Empty,
in-eclass: e ∈b X,
bfalse: ff,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Lemmas :
bag_size_empty_lemma,
top_wf
\mforall{}e,eo:Top. (e \mmember{}\msubb{} Empty \msim{} ff)
Date html generated:
2015_07_17-PM-00_42_48
Last ObjectModification:
2015_01_27-PM-11_09_06
Home
Index