Nuprl Definition : rel-comp
(R1 o R2) ==  λx,z. ∃y:B. ((R1 x y) ∧ (R2 y z))
Definitions occuring in Statement : 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
apply: f a
, 
lambda: λx.A[x]
Definitions occuring in definition : 
lambda: λx.A[x]
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
apply: f a
FDL editor aliases : 
rel-comp
Latex:
(R1  o  R2)  ==    \mlambda{}x,z.  \mexists{}y:B.  ((R1  x  y)  \mwedge{}  (R2  y  z))
Date html generated:
2019_06_20-PM-00_31_13
Last ObjectModification:
2019_03_27-PM-00_39_09
Theory : relations
Home
Index