Nuprl Definition : ss-function
ss-function(X;Y;f) == ∀x,x':Point(X). (x ≡ x' ⇒ f x ≡ f x')
Definitions occuring in Statement :
ss-eq: 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,
ss-eq: x ≡ y,
apply: f a
FDL editor aliases :
ss-function
Latex:
ss-function(X;Y;f) == \mforall{}x,x':Point(X). (x \mequiv{} x' {}\mRightarrow{} f x \mequiv{} f x')
Date html generated:
2019_10_31-AM-07_26_33
Last ObjectModification:
2019_03_19-PM-03_41_12
Theory : constructive!algebra
Home
Index