SubPrdXYZRS:=R∘S∩{x,z:xR⊆Sz}
RelationXYR
RelationYZS
Notation.
SubPrdXYZRS can be written SubPrdRS when X, Y and Z are clear from the context.
SubPrdRS can be written in symbols as R⊲S.
fun SubPrd(X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
R.S & { x: X, z: Z | x.R in S.z }
}
SupPrdXYZRS:=R∘S∩{x,z:xR⊇Sz}
RelationXYR
RelationYZS
Notation.
SupPrdXYZRS can be written SupPrdRS when X, Y and Z are clear from the context.
SupPrdRS can be written in symbols as R⊳S.
fun SupPrd(X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
R.S & { x: X, z: Z | S.z in x.R }
}
SqrPrdXYZRS:=R∘S∩{x,z:xR=Sz}
RelationXYR
RelationYZS
Notation.
SqrPrdXYZRS can be written SqrPrdRS when X, Y and Z are clear from the context.
SqrPrdRS can be written in symbols as R⋄S.
fun SqrPrd(X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
R.S & { x: X, z: Z | x.R = S.z }
}