Nuprl Definition : set-relation-on
SetRelationOn(A;R) == ∀x,x',y,y':{u:Set{i:l}| (u ∈ A)} . (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Definitions occuring in Statement :
setmem: (x ∈ s),
seteq: seteq(s1;s2),
Set: Set{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
apply: f a,
implies: P ⇒ Q,
seteq: seteq(s1;s2),
setmem: (x ∈ s),
Set: Set{i:l},
set: {x:A| B[x]} ,
all: ∀x:A. B[x]
FDL editor aliases :
set-relation-on
Latex:
SetRelationOn(A;R) ==
\mforall{}x,x',y,y':\{u:Set\{i:l\}| (u \mmember{} A)\} . (seteq(x;x') {}\mRightarrow{} seteq(y;y') {}\mRightarrow{} (R x y) {}\mRightarrow{} (R x' y'))
Date html generated:
2018_05_29-PM-01_51_45
Last ObjectModification:
2018_05_25-AM-10_28_22
Theory : constructive!set!theory
Home
Index