Nuprl Definition : set-relation
This says that the relation R respects the extensional equality ⌜seteq(x;y)⌝.⋅
SetRelation(R) == ∀x,x',y,y':Set{i:l}. (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Definitions occuring in Statement :
seteq: seteq(s1;s2),
Set: Set{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Definitions occuring in definition :
apply: f a,
implies: P ⇒ Q,
seteq: seteq(s1;s2),
Set: Set{i:l},
all: ∀x:A. B[x]
FDL editor aliases :
set-relation
Latex:
SetRelation(R) == \mforall{}x,x',y,y':Set\{i:l\}. (seteq(x;x') {}\mRightarrow{} seteq(y;y') {}\mRightarrow{} (R x y) {}\mRightarrow{} (R x' y'))
Date html generated:
2018_05_29-PM-01_51_39
Last ObjectModification:
2018_05_24-PM-06_08_29
Theory : constructive!set!theory
Home
Index