Nuprl Definition : l_all2
(∀x<y∈L.P[x; y]) == ∀x,y:T. (x before y ∈ L ⇒ P[x; y])
Definitions occuring in Statement :
l_before: x before y ∈ l,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
l_before: x 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