Nuprl Definition : bl-all
(∀x∈L.P[x])_b == reduce(λx,p. (P[x] ∧b p);tt;L)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
band: p ∧b q,
btrue: tt,
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
band: p ∧b q,
btrue: tt
FDL editor aliases :
bl-all
Latex:
(\mforall{}x\mmember{}L.P[x])\_b == reduce(\mlambda{}x,p. (P[x] \mwedge{}\msubb{} p);tt;L)
Date html generated:
2016_05_14-PM-02_09_09
Last ObjectModification:
2015_09_22-PM-05_55_23
Theory : list_1
Home
Index