Nuprl Definition : l-all-and
B ∧ ∀x∈L.P[x] ==  reduce(λx,p. (P[x] ∧ p);B;L)
Definitions occuring in Statement : 
reduce: reduce(f;k;as)
, 
and: P ∧ Q
, 
lambda: λx.A[x]
Definitions occuring in definition : 
reduce: reduce(f;k;as)
, 
lambda: λx.A[x]
, 
and: P ∧ Q
FDL editor aliases : 
l-all-and
Latex:
B  \mwedge{}  \mforall{}x\mmember{}L.P[x]  ==    reduce(\mlambda{}x,p.  (P[x]  \mwedge{}  p);B;L)
Date html generated:
2016_05_15-PM-03_46_48
Last ObjectModification:
2015_09_23-AM-07_44_45
Theory : general
Home
Index