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