Nuprl Definition : binrel_le

E ≡>{T} E' ==  ∀x,y:T.  ((E x y) ⇒ (E' x y))



Definitions occuring in Statement :  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a

Latex:
E  \mequiv{}>\{T\}  E'  ==    \mforall{}x,y:T.    ((E  x  y)  {}\mRightarrow{}  (E'  x  y))



Date html generated: 2016_05_14-PM-03_54_48
Last ObjectModification: 2015_09_22-PM-06_01_50

Theory : relations2


Home Index