---

X  Y:T ==  f:E(X)  E(Y). (f:X  Y:T  Surj(E(X);E(Y);f))

---

Definitions :  exists: x:A. B[x],  function: x:A  B[x],  and: P  Q,  es-fwd-propagation-via: f:X  Y:T,  surject: Surj(A;B;f),  es-E-interface: E(X)
FDL editor aliases :  es-propagate-iff1

---

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: 2010_08_27-PM-02_42_01
Last ObjectModification: 2009_12_16-AM-08_35_48

Home Index