Nuprl Definition : single-valued-classrel
single-valued-classrel(es;X;T) ==  ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))
Definitions occuring in Statement : 
classrel: v ∈ X(e), 
es-E: E, 
all: ∀x:A. B[x], 
implies: P ⇒ Q, 
equal: s = t ∈ T
FDL editor aliases : 
single-valued-classrel
Latex:
single-valued-classrel(es;X;T)  ==    \mforall{}e:E.  \mforall{}v1,v2:T.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))
Date html generated:
2016_05_16-PM-01_41_35
Last ObjectModification:
2012_02_25-PM-01_13_47
Theory : event-ordering
Home
Index