Nuprl Definition : cond_rel_implies

when P, R1 => R2 ==  ∀x,y:T.  ((P x)  (x R1 y)  (x R2 y))



Definitions occuring in Statement :  infix_ap: y all: x:A. B[x] implies:  Q apply: a
Definitions occuring in definition :  all: x:A. B[x] apply: a implies:  Q infix_ap: y
FDL editor aliases :  cond_rel_implies

Latex:
when  P,  R1  =>  R2  ==    \mforall{}x,y:T.    ((P  x)  {}\mRightarrow{}  (x  R1  y)  {}\mRightarrow{}  (x  R2  y))



Date html generated: 2016_05_13-PM-04_19_04
Last ObjectModification: 2015_09_22-PM-05_46_46

Theory : relations


Home Index