Nuprl Definition : coset-relation
coSetRelation(R) == ∀x,x',y,y':coSet{i:l}. (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
Definitions occuring in Statement :
seteq: seteq(s1;s2),
coSet: coSet{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),
coSet: coSet{i:l},
all: ∀x:A. B[x]
FDL editor aliases :
coset-relation
Latex:
coSetRelation(R) == \mforall{}x,x',y,y':coSet\{i:l\}. (seteq(x;x') {}\mRightarrow{} seteq(y;y') {}\mRightarrow{} (R x y) {}\mRightarrow{} (R x' y'))
Date html generated:
2018_07_29-AM-10_06_06
Last ObjectModification:
2018_07_20-PM-00_41_36
Theory : constructive!set!theory
Home
Index