Nuprl Definition : es-propagate-iff1
X 
⇐⇒ Y:T ==  ∃f:E(X) ⟶ E(Y). (f:X 
⇒ Y:T ∧ Surj(E(X);E(Y);f))
Definitions occuring in Statement : 
es-fwd-propagation-via: f:X 
⇒ Y:T
, 
es-E-interface: E(X)
, 
surject: Surj(A;B;f)
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
function: x:A ⟶ B[x]
FDL editor aliases : 
es-propagate-iff1
Latex:
X  \mLeftarrow{}{}\mRightarrow{}  Y:T  ==    \mexists{}f:E(X)  {}\mrightarrow{}  E(Y).  (f:X  {}\mRightarrow{}  Y:T  \mwedge{}  Surj(E(X);E(Y);f))
Date html generated:
2016_05_17-AM-06_46_06
Last ObjectModification:
2012_02_25-PM-02_27_17
Theory : event-ordering
Home
Index