Nuprl Definition : l_all2

(∀x<y∈L.P[x; y]) ==  ∀x,y:T.  (x before y ∈  P[x; y])



Definitions occuring in Statement :  l_before: before y ∈ l all: x:A. B[x] implies:  Q
Definitions occuring in definition :  all: x:A. B[x] implies:  Q l_before: before y ∈ l
FDL editor aliases :  l_all2

Latex:
(\mforall{}x<y\mmember{}L.P[x;  y])  ==    \mforall{}x,y:T.    (x  before  y  \mmember{}  L  {}\mRightarrow{}  P[x;  y])



Date html generated: 2016_05_15-PM-01_55_51
Last ObjectModification: 2015_09_23-AM-07_37_28

Theory : list!


Home Index