Nuprl Lemma : isallevents_lemma
∀e,eo:Top. (e ∈b E ~ tt)
Proof
Definitions occuring in Statement :
es-all-events: E,
in-eclass: e ∈b X,
btrue: tt,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
es-all-events: E,
in-eclass: e ∈b X,
all: ∀x:A. B[x],
member: t ∈ T,
top: Top,
eq_int: (i =z j)
Latex:
\mforall{}e,eo:Top. (e \mmember{}\msubb{} E \msim{} tt)
Date html generated:
2016_05_16-PM-02_46_36
Last ObjectModification:
2015_12_29-AM-11_23_56
Theory : event-ordering
Home
Index