Nuprl Definition : set-function
set-function{i:l}(s; x.f[x]) == ∀x,y:coSet{i:l}. ((x ∈ s) ⇒ (y ∈ s) ⇒ seteq(x;y) ⇒ seteq(f[x];f[y]))
Definitions occuring in Statement :
setmem: (x ∈ s),
seteq: seteq(s1;s2),
coSet: coSet{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
seteq: seteq(s1;s2),
implies: P ⇒ Q,
setmem: (x ∈ s),
coSet: coSet{i:l},
all: ∀x:A. B[x]
Latex:
set-function\{i:l\}(s; x.f[x]) ==
\mforall{}x,y:coSet\{i:l\}. ((x \mmember{} s) {}\mRightarrow{} (y \mmember{} s) {}\mRightarrow{} seteq(x;y) {}\mRightarrow{} seteq(f[x];f[y]))
Date html generated:
2018_07_29-AM-09_52_31
Last ObjectModification:
2018_07_18-PM-02_26_51
Theory : constructive!set!theory
Home
Index