Nuprl Definition : trans

(basic):: Trans(T;x,y.E[x; y]) ==  ∀a,b,c:T.  (E[a; b] ⇒ E[b; c] ⇒ E[a; c])


Definitions occuring in Statement :  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q
FDL editor aliases :  trans
Latex:
(basic)::  Trans(T;x,y.E[x;  y])  ==    \mforall{}a,b,c:T.    (E[a;  b]  {}\mRightarrow{}  E[b;  c]  {}\mRightarrow{}  E[a;  c])


Date html generated: 2016_05_13-PM-04_14_44
Last ObjectModification: 2015_09_22-PM-05_46_02

Theory : rel_1


Home Index