Nuprl Definition : utrans

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



Definitions occuring in Statement :  uall: [x:A]. B[x] implies:  Q
Definitions occuring in definition :  uall: [x:A]. B[x] implies:  Q
FDL editor aliases :  utrans

Latex:
(basic)::  UniformlyTrans(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_45
Last ObjectModification: 2015_09_22-PM-05_46_03

Theory : rel_1


Home Index