Nuprl Definition : ss-map
ss-map(X;Y;f) == ∀x,x':Point(X). (f x # f x' ⇒ x # x')
Definitions occuring in Statement :
ss-sep: x # y,
ss-point: Point(ss),
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
ss-point: Point(ss),
implies: P ⇒ Q,
apply: f a,
ss-sep: x # y
FDL editor aliases :
ss-map
Latex:
ss-map(X;Y;f) == \mforall{}x,x':Point(X). (f x \# f x' {}\mRightarrow{} x \# x')
Date html generated:
2019_10_31-AM-07_26_28
Last ObjectModification:
2019_03_19-PM-03_40_53
Theory : constructive!algebra
Home
Index