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
Definitions unfolded in proof :
es-empty-interface: Empty,
in-eclass: e ∈b X,
eq_int: (i =z j),
all: ∀x:A. B[x],
member: t ∈ T
Latex:
\mforall{}e,eo:Top. (e \mmember{}\msubb{} Empty \msim{} ff)
Date html generated:
2016_05_16-PM-02_24_01
Last ObjectModification:
2015_12_29-AM-11_41_45
Theory : event-ordering
Home
Index