Nuprl Definition : es-fwd-propagation
X ⇒ Y:T == ∃f:E(X) ─→ E(Y). f:X ⇒ Y:T
Definitions occuring in Statement :
es-fwd-propagation-via: f:X ⇒ Y:T,
es-E-interface: E(X),
exists: ∃x:A. B[x],
function: x:A ─→ B[x]
FDL editor aliases :
es-fwd-propagation
Latex:
X {}\mRightarrow{} Y:T == \mexists{}f:E(X) {}\mrightarrow{} E(Y). f:X {}\mRightarrow{} Y:T
Date html generated:
2015_07_21-PM-03_27_32
Last ObjectModification:
2012_02_25-PM-02_27_01
Home
Index