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