Nuprl Definition : topfun
topfun(X;Y) == {f:|X| ⟶ |Y|| ∀a,b:|X|. (topeq(X;a;b) ⇒ topeq(Y;f a;f b))}
Definitions occuring in Statement :
topeq: topeq(X;a;b),
toptype: |X|,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
apply: f a,
topeq: topeq(X;a;b),
implies: P ⇒ Q,
toptype: |X|,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
topfun
Latex:
topfun(X;Y) == \{f:|X| {}\mrightarrow{} |Y|| \mforall{}a,b:|X|. (topeq(X;a;b) {}\mRightarrow{} topeq(Y;f a;f b))\}
Date html generated:
2018_07_29-AM-09_48_10
Last ObjectModification:
2018_06_21-AM-10_06_51
Theory : inner!product!spaces
Home
Index