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:
2015_07_21-PM-03_27_52
Last ObjectModification:
2012_02_25-PM-02_27_17
Home
Index